leodemoura on no_type_class_dep_at_unifier
experiment (compare)
leodemoura on master
chore: simplify README (compare)
leodemoura on master
chore: update README (compare)
theorem ext (A B : Hom K V W) (HAB : ∀ v, A.T v = B.T v) : A = B :=
begin
cases A,
cases B,
congr,
apply funext,
simp [T] at HAB,
exact HAB
end
The whole library didn't exist only a few months ago
add_comm_group
requires what I call zero_add
and add_zero
when one of them is enough?
zero_add
that is enough
add_monoid
and there it definitely can't be derived
(-)
doesn't work
has_neg.neg
is too long
neg
first and then instance : has_neg := \<neg\>
protected meta def transfer_core : tactic unit := do
transfer.transfer [`relator.rel_forall_of_total, `relator.rel_not,
`int.rel_eq, `int.rel_zero, `int.rel_one,
`int.rel_add, `int.rel_neg, `int.rel_mul]
protected meta def transfer (distrib := tt) : tactic unit :=
if distrib then `[int.transfer_core, simp [add_mul, mul_add]]
else `[int.transfer_core, simp]
instance : comm_ring int :=
{ add := int.add,
add_assoc := by int.transfer,
zero := int.zero,
zero_add := by int.transfer,
add_zero := by int.transfer,
neg := int.neg,
add_left_neg := by int.transfer,
add_comm := by int.transfer,
mul := int.mul,
mul_assoc := by int.transfer tt,
one := int.one,
one_mul := by int.transfer,
mul_one := by int.transfer,
left_distrib := by int.transfer tt,
right_distrib := by int.transfer tt,
mul_comm := by int.transfer}
protected meta def