inductive Paramodulator.Node : Type

• nil : Node
• pair : Node → Node → Node

@[instance_reducible]

instance Paramodulator.instDecidableEqNode : DecidableEq Node

Equations

• Paramodulator.instDecidableEqNode = Paramodulator.instDecidableEqNode.decEq

def Paramodulator.instDecidableEqNode.decEq (x✝ x✝¹ : Node) : Decidable (x✝ = x✝¹)

Equations

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

def Lean.Parser.Category.node : Category

Equations

• Lean.Parser.Category.node = { }

def Paramodulator.node.quot : Lean.ParserDescr

Equations

• Paramodulator.node.quot = Lean.ParserDescr.node `Lean.Parser.Term.quot 1024 (Lean.ParserDescr.node `node.quot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "`(node| ") (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `node 0) (Lean.ParserDescr.symbol ")"))))

def Paramodulator.node_ : Lean.ParserDescr

Equations

• Paramodulator.node_ = Lean.ParserDescr.node `Paramodulator.node_ 1022 (Lean.ParserDescr.const `num)

def Paramodulator.node__1 : Lean.ParserDescr

Equations

• Paramodulator.node__1 = Lean.ParserDescr.node `Paramodulator.node__1 1022 (Lean.ParserDescr.const `ident)

def Paramodulator.node__ : Lean.TrailingParserDescr

Equations

• Paramodulator.node__ = Lean.ParserDescr.trailingNode `Paramodulator.node__ 1022 0 (Lean.ParserDescr.cat `node 0)

def Paramodulator.«node(_)» : Lean.ParserDescr

Equations

• Paramodulator.«node(_)» = Lean.ParserDescr.node `Paramodulator.«node(_)» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "(") (Lean.ParserDescr.cat `node 0)) (Lean.ParserDescr.symbol ")"))

def Paramodulator.term!!_ : Lean.ParserDescr

Equations

• Paramodulator.term!!_ = Lean.ParserDescr.node `Paramodulator.term!!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!!") (Lean.ParserDescr.cat `node 0))

@[instance_reducible]

instance Paramodulator.instZeroNode : Zero Node

Equations

• Paramodulator.instZeroNode = { zero := Paramodulator.Node.nil }

@[instance_reducible]

instance Paramodulator.instOneNode : One Node

Equations

• Paramodulator.instOneNode = { one := Paramodulator.Node.pair 0 0 }

def Paramodulator.const (n : ℕ) : Node

Equations

• Paramodulator.const 0 = 1
• Paramodulator.const n_2.succ = Paramodulator.Node.pair 0 (Paramodulator.const n_2)

def Paramodulator.Node.left (x : Node) : Node

Equations

• (x_2.pair a).left = x_2
• x.left = 0

def Paramodulator.Node.right (x : Node) : Node

Equations

• (x_2.pair a).right = a
• x.right = 0