Documentation

Init.LawfulBEqTactics

source
def DerivingHelpers.tacticDeriving_ReflEq_tactic :
Lean.ParserDescr
Equations
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
    Instances For
      source
      def tacticDeriving_LawfulEq_tactic :
      Lean.ParserDescr
      Equations
      Instances For