michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(hott): remove unnecessary '[trans]' attributes

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-02 21:35:59 -07:00
parent 326048df54
commit 657ad3327f
2 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/equiv.hlean
View file

@ -273,7 +273,5 @@ namespace equiv
attribute equiv.trans [trans] attribute equiv.trans [trans]
attribute equiv.refl [refl] attribute equiv.refl [refl]
attribute equiv.symm [symm] attribute equiv.symm [symm]
attribute equiv_of_equiv_of_eq [trans]
attribute equiv_of_eq_of_equiv [trans]
end equiv end equiv

3
hott/init/logic.hlean
View file

@ -125,9 +125,6 @@ section
assume H₁ H₂, H₂ ▸ H₁ assume H₁ H₂, H₂ ▸ H₁
end end
attribute ne.of_eq_of_ne [trans]
attribute ne.of_ne_of_eq [trans]
/- iff -/ /- iff -/
definition iff (a b : Type) := prod (a → b) (b → a) definition iff (a b : Type) := prod (a → b) (b → a)