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 α] :

add = HAdd.hAdd

theorem Sub.sub_eq_hSub {α : Type u_1} [Sub α] :

sub = HSub.hSub

theorem Mul.mul_eq_hMul {α : Type u_1} [Mul α] :

mul = HMul.hMul

theorem Div.div_eq_hDiv {α : Type u_1} [Div α] :

div = HDiv.hDiv

theorem Mod.mod_eq_hMod {α : Type u_1} [Mod α] :

mod = HMod.hMod

theorem Pow.pow_eq_hPow {α : Type u_1} {β : Type u_2} [Pow α β] :

pow = HPow.hPow

theorem SMul.smul_eq_hSMul {α : Type u_1} {β : Type u_2} [SMul α β] :

smul = HSMul.hSMul

theorem Mul.mul_eq_smul {α : Type u_1} [Mul α] :

mul = SMul.smul

theorem Append.append_eq_hAppend {α : Type u_1} [Append α] :

append = HAppend.hAppend

theorem OrElse.orElse_eq_hOrElse {α : Type u_1} [OrElse α] :

orElse = HOrElse.hOrElse

theorem AndThen.andThen_eq_hAndThen {α : Type u_1} [AndThen α] :

andThen = HAndThen.hAndThen

theorem AndOp.andOp_hAnd {α : Type u_1} [AndOp α] :

and = HAnd.hAnd

theorem XorOp.xor_hXor {α : Type u_1} [XorOp α] :

xor = HXor.hXor

theorem OrOp.or_hOr {α : Type u_1} [OrOp α] :

theorem ShiftLeft.shiftLeft_hShiftLeft {α : Type u_1} [ShiftLeft α] :

shiftLeft = HShiftLeft.hShiftLeft

theorem ShiftRight.shiftRight_hShiftRight {α : Type u_1} [ShiftRight α] :

shiftRight = HShiftRight.hShiftRight