source
def DerivingHelpers.tacticDeriving_ReflEq_tactic :
Lean.ParserDescr
Equations

- DerivingHelpers.tacticDeriving_ReflEq_tactic = Lean.ParserDescr.node `DerivingHelpers.tacticDeriving_ReflEq_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "deriving_ReflEq_tactic" false)

Instances For

source
theorem DerivingHelpers.and_true_curry {a b : Bool} {P : Prop} (h : a = true → b = true → P) :
(a && b) = true → P
source
theorem DerivingHelpers.deriving_lawful_beq_helper_dep {α : Type u_1} {x y : α} [BEq α] [ReflBEq α] {t : (x == y) = true → Bool} {P : Prop} (inst : (x == y) = true → x = y) (k : ∀ (h : x = y), t ⋯ = true → P) :
(if h : (x == y) = true then t h else false) = true → P
source
theorem DerivingHelpers.deriving_lawful_beq_helper_nd {α : Type u_1} {x y : α} [BEq α] [ReflBEq α] {P : Prop} (inst : (x == y) = true → x = y) (k : x = y → P) :
(x == y) = true → P
source
def tacticDeriving_LawfulEq_tactic_step :
Lean.ParserDescr
Equations

- tacticDeriving_LawfulEq_tactic_step = Lean.ParserDescr.node `tacticDeriving_LawfulEq_tactic_step 1024 (Lean.ParserDescr.nonReservedSymbol "deriving_LawfulEq_tactic_step" false)

Instances For

source
def tacticDeriving_LawfulEq_tactic :
Lean.ParserDescr
Equations

- tacticDeriving_LawfulEq_tactic = Lean.ParserDescr.node `tacticDeriving_LawfulEq_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "deriving_LawfulEq_tactic" false)

Instances For