class Reduce (α : Type u) (β : outParam (Type v)) : Type (max u v)

• reducing : α → β

class Abort (α : Type u) (β : outParam (Type v)) : Type (max u v)

• abort : α → β

class Diverge (α : Type u) (β : outParam (Type v)) : Type (max u v)

• div : α → β

class Block (α : Type u) (β : outParam (Type v)) : Type (max u v)

• block : α → β

def «term⟦_⟧*» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term⟦_⟧⊥» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term⟦_⟧∞» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term⟦_⟧⊘» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.