Documentation

Init.MethodSpecsSimp

This module contains theorems to be added to the @[method_specs_simp] simpset. When we use the idiom of a heterogeneous class with notation (e.g. HAppend) and a homogeneous class that the user typically instantiates, these rewrite the method specifications generated by @[method_specs] from the homogeneous form to the desired heterogeneous form.

Should modules within Init use @[method_specs] on such instances, they should import this file.

theorem Add.add_eq_hAdd {α : Type u} [inst : Add α] :
theorem Sub.sub_eq_hSub {α : Type u_1} [Sub α] :
theorem Mul.mul_eq_hMul {α : Type u_1} [Mul α] :
theorem Div.div_eq_hDiv {α : Type u_1} [Div α] :
theorem Mod.mod_eq_hMod {α : Type u_1} [Mod α] :
theorem Pow.pow_eq_hPow {α : Type u_1} {β : Type u_2} [Pow α β] :
theorem SMul.smul_eq_hSMul {α : Type u_1} {β : Type u_2} [SMul α β] :
theorem Mul.mul_eq_smul {α : Type u_1} [Mul α] :
theorem AndOp.andOp_hAnd {α : Type u_1} [AndOp α] :
theorem XorOp.xor_hXor {α : Type u_1} [XorOp α] :
theorem OrOp.or_hOr {α : Type u_1} [OrOp α] :