inductive Expr : Type

• nil : Expr
• pair : Expr → Expr → Expr

@[instance_reducible]

instance instInhabitedExpr : Inhabited Expr

Equations

• instInhabitedExpr = { default := instInhabitedExpr.default }

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

Equations

• instDecidableEqExpr.decEq Expr.nil Expr.nil = isTrue ⋯
• instDecidableEqExpr.decEq Expr.nil (a.pair a_1) = isFalse ⋯
• instDecidableEqExpr.decEq (a.pair a_1) Expr.nil = isFalse ⋯
• instDecidableEqExpr.decEq (a.pair a_1) (b.pair b_1) = if h : a = b then h ▸ have inst := instDecidableEqExpr.decEq a a; have inst := instDecidableEqExpr.decEq a_1 b_1; if h : a_1 = b_1 then h ▸ have inst := instDecidableEqExpr.decEq a_1 a_1; isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqExpr : DecidableEq Expr

Equations

• instDecidableEqExpr = instDecidableEqExpr.decEq

def Expr.isNil (a : Expr) : Prop

Equations

• Expr.nil.isNil = True
• a.isNil = False

def Expr.isPair (a : Expr) : Prop

Equations

• Expr.nil.isPair = False
• a.isPair = True

@[instance_reducible]

instance Expr.instDecidableIsNil {a : Expr} : Decidable a.isNil

Equations

• Expr.instDecidableIsNil = isTrue True.intro
• Expr.instDecidableIsNil = isFalse Expr.instDecidableIsNil._proof_1

@[instance_reducible]

instance Expr.instDecidableIsPair {a : Expr} : Decidable a.isPair

Equations

• Expr.instDecidableIsPair = isFalse Expr.instDecidableIsNil._proof_1
• Expr.instDecidableIsPair = isTrue True.intro

@[instance_reducible]

instance Expr.instCoeSortProp : CoeSort Expr Prop

Equations

• Expr.instCoeSortProp = { coe := Expr.isPair }

def Expr.fst (a : Expr) : Expr

Equations

• Expr.nil.fst = Expr.nil
• (a_2.pair a_3).fst = a_2

def Expr.snd (a : Expr) : Expr

Equations

• Expr.nil.snd = Expr.nil
• (a_2.pair a_3).snd = a_3

def Expr.toPair (a : Expr) : Expr

Equations

• a.toPair = a.fst.pair a.snd

def Expr.ite (a b c : Expr) : Expr

Equations

• a.ite b c = if a.isPair then b else c

def Expr.T : Expr

Equations

• Expr.T = Expr.nil.pair Expr.nil

def Expr.F : Expr

Equations

• Expr.F = Expr.nil

def Expr.toProp (a : Expr) : Expr

Equations

• a.toProp = a.ite Expr.T Expr.F

def Expr.not (a : Expr) : Expr

Equations

• a.not = a.ite Expr.F Expr.T

def Expr.imp (a b : Expr) : Expr

Equations

• a.imp b = a.ite b.toProp Expr.T

def Expr.or (a b : Expr) : Expr

Equations

• a.or b = a.ite Expr.T b.toProp

def Expr.and (a b : Expr) : Expr

Equations

• a.and b = a.ite b.toProp Expr.F

def Expr.iff (a b : Expr) : Expr

Equations

• a.iff b = a.ite b.toProp b.not

def Expr.eq (a b : Expr) : Expr

Equations

• a.eq b = if a = b then Expr.T else Expr.F

def Expr.sle (a b : Expr) : Expr

Equations

• Expr.nil.sle b = if Expr.nil = b then Expr.T else Expr.T
• a.sle Expr.nil = if a = Expr.nil then Expr.T else Expr.F
• a.sle (x_1.pair y) = if a = x_1.pair y then Expr.T else (a.sle x_1).or (a.sle y)

def Expr.slt (a b : Expr) : Expr

Equations

• a.slt Expr.nil = Expr.F
• a.slt (a_2.pair a_3) = (a.sle a_2).or (a.sle a_3)

def Expr.depth' (a : Expr) : ℕ

Equations

• Expr.nil.depth' = 0
• (a_2.pair a_3).depth' = 1 + max a_2.depth' a_3.depth'

@[instance_reducible]

instance Expr.instLE : LE Expr

Equations

• Expr.instLE = { le := fun (a b : Expr) => (a.sle b).isPair }

@[instance_reducible]

instance Expr.instLT : LT Expr

Equations

• Expr.instLT = { lt := fun (a b : Expr) => (a.slt b).isPair }

@[instance_reducible]

instance Expr.instDecidableLE : DecidableLE Expr

Equations

• a.instDecidableLE b = Expr.instDecidableIsPair

@[instance_reducible]

instance Expr.instDecidableLT : DecidableLT Expr

Equations

• a.instDecidableLT b = Expr.instDecidableIsPair