Commit 2021-09-15 13:22 f8d8171d

View on Github →

refactor(logic/relator): turn *_unique and *_total into defs, not classes (#9135) We had (almost) no instances for these classes and (almost) no lemmas taking these assumptions as TC arguments.

Estimated changes

Modified src/computability/turing_machine.lean

Modified src/data/list/forall2.lean

deleted theorem list.bi_unique_forall₂

deleted theorem list.left_unique_forall₂

deleted theorem list.right_unique_forall₂

added theorem relator.bi_unique.forall₂

added theorem relator.left_unique.forall₂

added theorem relator.right_unique.forall₂

Modified src/data/list/perm.lean

Modified src/data/option/basic.lean

Modified src/data/part.lean

Modified src/data/seq/computation.lean

Modified src/logic/relation.lean

Modified src/logic/relator.lean

added theorem relator.bi_total.rel_exists

added theorem relator.bi_total.rel_forall

added def relator.bi_total

added theorem relator.bi_total_eq

added def relator.bi_unique

added theorem relator.left_total.rel_exists

added def relator.left_total

added theorem relator.left_unique.flip

deleted theorem relator.left_unique.unique

added def relator.left_unique

deleted theorem relator.left_unique_flip

deleted theorem relator.rel_exists_of_left_total

deleted theorem relator.rel_exists_of_total

deleted theorem relator.rel_forall_of_right_total

deleted theorem relator.rel_forall_of_total

added theorem relator.right_total.rel_forall

added def relator.right_total

deleted theorem relator.right_unique.unique

added def relator.right_unique