inductive SK.Expr : Type

• K : Expr
• S : Expr
• App : Expr → Expr → Expr

@[instance_reducible]

instance SK.instInhabitedExpr : Inhabited Expr

Equations

• SK.instInhabitedExpr = { default := SK.instInhabitedExpr.default }

@[instance_reducible]

instance SK.instDecidableEqExpr : DecidableEq Expr

Equations

• SK.instDecidableEqExpr = SK.instDecidableEqExpr.decEq

def SK.instDecidableEqExpr.decEq (x✝ x✝¹ : Expr) : Decidable (x✝ = x✝¹)

Equations

• SK.instDecidableEqExpr.decEq SK.Expr.K SK.Expr.K = isTrue ⋯
• SK.instDecidableEqExpr.decEq SK.Expr.K SK.Expr.S = isFalse SK.instDecidableEqExpr.decEq._proof_1
• SK.instDecidableEqExpr.decEq SK.Expr.K (a %% a_1) = isFalse ⋯
• SK.instDecidableEqExpr.decEq SK.Expr.S SK.Expr.K = isFalse SK.instDecidableEqExpr.decEq._proof_3
• SK.instDecidableEqExpr.decEq SK.Expr.S SK.Expr.S = isTrue ⋯
• SK.instDecidableEqExpr.decEq SK.Expr.S (a %% a_1) = isFalse ⋯
• SK.instDecidableEqExpr.decEq (a %% a_1) SK.Expr.K = isFalse ⋯
• SK.instDecidableEqExpr.decEq (a %% a_1) SK.Expr.S = isFalse ⋯
• SK.instDecidableEqExpr.decEq (a %% a_1) (b %% b_1) = if h : a = b then h ▸ have inst := SK.instDecidableEqExpr.decEq a a; have inst := SK.instDecidableEqExpr.decEq a_1 b_1; if h : a_1 = b_1 then h ▸ have inst := SK.instDecidableEqExpr.decEq a_1 a_1; isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance SK.instReprExpr : Repr Expr

Equations

• SK.instReprExpr = { reprPrec := SK.instReprExpr.repr }

def SK.instReprExpr.repr : Expr → ℕ → Std.Format

Equations

• SK.instReprExpr.repr SK.Expr.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SK.Expr.K")).group prec✝
• SK.instReprExpr.repr SK.Expr.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SK.Expr.S")).group prec✝
• SK.instReprExpr.repr (a %% a_1) prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SK.Expr.App" ++ Std.Format.line ++ SK.instReprExpr.repr a 1024 ++ Std.Format.line ++ SK.instReprExpr.repr a_1 1024)).group prec✝

def SK.«term_%%_» : Lean.TrailingParserDescr

Equations

• SK.«term_%%_» = Lean.ParserDescr.trailingNode `SK.«term_%%_» 1000 1000 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " %% ") (Lean.ParserDescr.cat `term 1001))

def SK.I : Expr

Equations

• SK.I = SK.Expr.S %% SK.Expr.K %% SK.Expr.K

inductive SK.Reduces : Expr → Expr → Prop

• rfl {a : Expr} : Reduces a a
• trans {a b c : Expr} : Reduces a b → Reduces b c → Reduces a c
• app {a b a' b' : Expr} : Reduces a a' → Reduces b b' → Reduces (a %% b) (a' %% b')
• k {a b : Expr} : Reduces (Expr.K %% a %% b) a
• s {a b c : Expr} : Reduces (Expr.S %% a %% b %% c) (a %% c %% (b %% c))

inductive SK.ExprNe : Expr → Expr → Prop

• comb : ExprNe Expr.K Expr.S
• reduce {a b a' b' : Expr} : Reduces a a' → Reduces b b' → ExprNe a' b' → ExprNe a b
• ext {a b c x y : Expr} : Reduces (a %% c) x → Reduces (b %% c) y → ExprNe x y → ExprNe a b

def SK.ExprEq (a b : Expr) : Prop

Equations

• SK.ExprEq a b = ¬SK.ExprNe a b

class SK.Reduced (a : Expr) : Prop

• h {b : Expr} : Reduces a b → a = b

def SK.KI : Expr

Equations

• SK.KI = SK.Expr.K %% SK.I

def SK.KK : Expr

Equations

• SK.KK = SK.Expr.K %% SK.Expr.K