Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-20 22:50 c1e594bc

View on Github →

feat(meta, logic, tactic): lean 3.4.2: migrate coinductive_predicates, transfer, relator (#610)

Estimated changes

Modified leanpkg.toml

Modified src/data/list/defs.lean

Modified src/logic/relator.lean

added def relator.bi_total

added def relator.left_total

added def relator.left_unique

added theorem relator.left_unique_of_rel_eq

added def relator.lift_fun

added theorem relator.rel_exists_of_left_total

added theorem relator.rel_exists_of_total

added theorem relator.rel_forall_of_right_total

added theorem relator.rel_forall_of_total

added theorem relator.rel_imp

added theorem relator.rel_not

added def relator.right_total

added def relator.right_unique

Created src/meta/coinductive_predicates.lean

added theorem monotonicity.and

added theorem monotonicity.const

added theorem monotonicity.exists

added theorem monotonicity.false

added theorem monotonicity.imp

added theorem monotonicity.not

added theorem monotonicity.or

added theorem monotonicity.pi

added theorem monotonicity.true

added def name.last_string

Modified src/tactic/alias.lean

Modified src/tactic/explode.lean

Modified src/tactic/mk_iff_of_inductive_prop.lean

Created src/tactic/transfer.lean

Created tests/coinductive.lean

added inductive all_list

added theorem monotonicity.all_list