Commit 2022-11-22 07:59 1292163f

View on Github →

feat: add fun x ↦ t syntax (#617)

Estimated changes

modified theorem div_left_injective
modified theorem div_right_injective
modified theorem leftInverse_div_mul_left
modified theorem leftInverse_inv
modified theorem leftInverse_mul_left_div
modified theorem mul_right_surjective
modified theorem rightInverse_inv
modified def leftMul
modified theorem mul_left_injective
modified theorem mul_right_injective
modified def rightMul
modified theorem Bool.not_ne_id
modified theorem Fin.gt_wf
modified theorem FunLike.coe_eq_coe_fn
modified theorem FunLike.coe_injective
modified theorem EquivLike.inv_injective
modified theorem Int.coe_nat_strictMono
modified theorem List.append_left_injective
modified theorem List.append_right_injective
modified theorem List.chain_succ_range'
modified def List.finRange
modified theorem Option.coe_def
modified theorem Option.elim_none_some
modified theorem Option.map_injective'
modified theorem Option.none_orElse'
modified theorem Option.orElse_eq_none'
modified theorem Option.orElse_none'
modified theorem Option.pbind_eq_bind
modified theorem Option.some_injective
modified theorem Option.some_orElse'
modified theorem Prod.id_prod
modified theorem Prod.map_def
modified def Prod.swap
modified theorem true_equivalence
modified theorem Subtype.coe_injective
modified def Subtype.coind
modified theorem Sum.inl_injective
modified theorem Sum.inr_injective
modified theorem Fin.ne_of_vne
modified theorem Fin.vne_of_ne
modified theorem Function.injective_id
modified theorem not_of_eq_false
modified theorem not_or_of_not
modified theorem dite_eq_ite
modified theorem dite_eq_left_iff
modified theorem dite_eq_right_iff
modified theorem dite_ne_left_iff
modified theorem dite_ne_right_iff
modified theorem exists_unique_false
modified theorem fact_iff
modified theorem forall_or_of_or_forall
modified theorem Function.Injective.of_comp
modified theorem Function.Injective2.left'
modified theorem Function.Injective2.right'
modified theorem Function.Surjective.of_comp
modified theorem Function.const_def
modified theorem Function.const_injective
modified def Function.extend
modified theorem Function.extend_injective
modified theorem Function.id_def
modified theorem Function.uncurry_def
modified theorem Function.update_injective
modified theorem Function.iterate_commute
modified theorem List.foldr_const
modified theorem IsRefl.reflexive
modified theorem Reflexive.comap
modified def Relation.Join
modified theorem Relation.reflexive_join
modified theorem Relation.symmetric_join
modified theorem Symmetric.comap
modified theorem Eq.not_lt
modified theorem le_Prop_eq
modified theorem lt_of_le_of_ne'
modified theorem ne_of_not_le
modified theorem not_lt_of_le
modified theorem Function.const_mono
modified theorem List.foldl_monotone
modified theorem List.foldl_strictMono
modified theorem StrictMono.id_le
modified theorem Subtype.mono_coe
modified theorem antitone_app
modified theorem antitone_const
modified theorem antitone_lam
modified theorem monotoneOn_id
modified theorem monotone_app
modified theorem monotone_const
modified theorem monotone_fst
modified theorem monotone_id
modified theorem monotone_lam
modified theorem monotone_snd
modified theorem strictMonoOn_id
modified theorem strictMono_id
modified theorem Sat.Clause.reify_zero
modified theorem Sat.Fmla.subsumes_self