Remove relators and the transfer tactic

leanprover / lean3

Lean Theorem Prover

http://leanprover.github.io/

Apache License 2.0

2.15k stars 217 forks source link

Closed gebner closed 5 years ago

gebner commented 5 years ago

There are two motivations behind this removal:

@johoelzl and @cipher1024 want to develop the transfer tactic further inside of mathlib.
The ⇒ notation that we want to use for functors in category theory is currently used by relators.

Many of the int proofs were by transfer; this PR just restores the previous proofs.