Free (total) combinatory algebra

inductive FreeCA.Expr : Type

The underlying expressions fo the free combinatory algebra

• K: FreeCA.Expr
• S: FreeCA.Expr
• app: FreeCA.Expr → FreeCA.Expr → FreeCA.Expr

instance FreeCA.exprHasDot : HasDot FreeCA.Expr

Equations

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

inductive FreeCA.eq : FreeCA.Expr → FreeCA.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 : FreeCA.Expr}, a ≈ a
• app: ∀ {a b c d : FreeCA.Expr}, a ≈ b → c ≈ d → a ⬝ c ≈ b ⬝ d
• K: ∀ {a b : FreeCA.Expr}, (FreeCA.Expr.K.app a).app b ≈ a
• S: ∀ {a b c : FreeCA.Expr}, ((FreeCA.Expr.S.app a).app b).app c ≈ (a.app c).app (b.app c)

def 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

• FreeCA.«term_≈_» = Lean.ParserDescr.trailingNode `FreeCA.«term_≈_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 41))

@[reducible]

def FreeCA.carrier : Type

The carrier of the free total combinatory algebra

Equations

• FreeCA.carrier = Quot FreeCA.eq

@[reducible]

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

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

Equations

• FreeCA.mk = Quot.mk FreeCA.eq

instance FreeCA.hasDot : HasDot FreeCA.carrier

Equations

• FreeCA.hasDot = { dot := Quot.lift₂ (fun (x y : FreeCA.Expr) => FreeCA.mk (x ⬝ y)) FreeCA.hasDot.proof_1 FreeCA.hasDot.proof_2 }

@[simp]

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

instance FreeCA : CA FreeCA.carrier

The free combinatory algebra

Equations

• FreeCA = CA.mk (FreeCA.mk FreeCA.Expr.K) (FreeCA.mk FreeCA.Expr.S) FreeCA.proof_1 FreeCA.proof_2