Free (total) combinatory algebra

inductive LeanPool.PartialCombinatoryAlgebras.FreeCA.Expr : Type

The underlying expressions fo the free combinatory algebra

• K : Expr
• S : Expr
• app : Expr → Expr → Expr

@[implicit_reducible]

instance LeanPool.PartialCombinatoryAlgebras.FreeCA.exprHasDot : HasDot Expr

Equations

• LeanPool.PartialCombinatoryAlgebras.FreeCA.exprHasDot = { dot := LeanPool.PartialCombinatoryAlgebras.FreeCA.Expr.app }

inductive LeanPool.PartialCombinatoryAlgebras.FreeCA.eq : Expr → Expr → Prop

The equational axioms of the free combinatory algebra. Symmetry and transitivity are commented out because so far we have not needed them.

• refl {a : Expr} : a ≈ a
• app {a b c d : Expr} : a ≈ b → c ≈ d → a ⬝ c ≈ b ⬝ d
• K {a b : Expr} : (Expr.K.app a).app b ≈ a
• S {a b c : Expr} : ((Expr.S.app a).app b).app c ≈ (a.app c).app (b.app c)

def LeanPool.PartialCombinatoryAlgebras.FreeCA.«term_≈_» : Lean.TrailingParserDescr

The equational axioms of the free combinatory algebra. Symmetry and transitivity are commented out because so far we have not needed them.

Equations

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

@[reducible]

def LeanPool.PartialCombinatoryAlgebras.FreeCA.carrier : Type

The carrier of the free total combinatory algebra

Equations

• LeanPool.PartialCombinatoryAlgebras.FreeCA.carrier = Quot LeanPool.PartialCombinatoryAlgebras.FreeCA.eq

@[reducible]

def LeanPool.PartialCombinatoryAlgebras.FreeCA.mk (a : Expr) : Quot eq

Convert an expression to a (defined) partial element of the carrier.

Equations

• LeanPool.PartialCombinatoryAlgebras.FreeCA.mk = Quot.mk LeanPool.PartialCombinatoryAlgebras.FreeCA.eq

@[implicit_reducible]

instance LeanPool.PartialCombinatoryAlgebras.FreeCA.hasDot : HasDot carrier

Equations

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.FreeCA.eq_mk_app (a b : Expr) : mk a ⬝ mk b = mk (a ⬝ b)

@[implicit_reducible]

instance LeanPool.PartialCombinatoryAlgebras.FreeCA : CA FreeCA.carrier

The free combinatory algebra

Equations

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