Commit 2022-10-24 02:02 bc191fef

View on Github →

feat: align init.{core, logic} (#490) With this, the files init.core and init.logic are synchronized, although we aren't currently tracking files from init in port-status.

Estimated changes

modified theorem List.pairwise_append_comm
modified theorem List.pairwise_middle
modified theorem List.Perm.pairwise_iff
modified def String.isPrefix
modified def String.isSuffix
modified theorem min_left_comm
added inductive BinTree
added def Combinator.I
added def Combinator.K
added def Combinator.S
added def Prod.mk.injArrow
added def Std.Prec.arrow
added def Std.Prec.max
added def Std.Prec.maxPlus
added def Std.Priority.max
added def AntiSymmetric
added def AsFalse
added theorem AsTrue.get
added def AsTrue
added def Associative
added def Commutative
added def EmptyRelation
modified theorem ExistsUnique.elim
modified theorem ExistsUnique.intro
deleted theorem Iff.elim_left
deleted theorem Iff.elim_right
added theorem Implies.trans
added def Implies
added theorem InvImage.irreflexive
added theorem InvImage.trans
added def Irreflexive
added def IsDecEq
added def IsDecRefl
added def LeftCancelative
added def LeftCommutative
added def LeftDistributive
added def LeftIdentity
modified theorem Ne.def
added def NonContradictory
added def Reflexive
added def RightCancelative
added def RightCommutative
added def RightIdentity
modified def RightInverse
added def Symmetric
added def Total
added def Transitive
added def Xor'
added theorem and_assoc'
added theorem and_comm'
added theorem and_false_iff
added theorem and_self_iff
added theorem and_true_iff
deleted def anti_symmetric
deleted def as_false
deleted def as_true
deleted def associative
modified theorem cast_proof_irrel
deleted def commutative
modified theorem decidable_eq_inl_refl
modified theorem decidable_eq_inr_neg
added theorem decide_False'
added theorem decide_True'
modified theorem dif_ctx_congr
modified theorem dif_ctx_simp_congr
deleted def empty_relation
added theorem eq_rec_compose
deleted def equivalence
modified theorem exists_of_exists_unique
modified theorem exists_unique_congr
added theorem false_and_iff
added theorem false_iff_iff
added theorem false_or_iff
modified theorem heq_of_eq_rec_left
modified theorem heq_of_eq_rec_right
modified theorem if_congr
modified theorem if_congr_prop
modified theorem if_ctx_congr
modified theorem if_ctx_congr_prop
modified theorem if_ctx_simp_congr_prop
modified theorem if_simp_congr_prop
added theorem if_t_t
added theorem iff_false_iff
added theorem iff_self_iff
added theorem iff_true_iff
modified theorem imp_of_if_neg
modified theorem imp_of_if_pos
deleted theorem inv_image.irreflexive
deleted theorem inv_image.trans
deleted def inv_image
deleted def irreflexive
deleted def is_dec_eq
deleted def is_dec_refl
deleted def left_cancelative
modified theorem left_comm
deleted def left_commutative
deleted def left_distributive
deleted def left_identity
modified theorem let_body_eq
modified theorem let_eq
modified theorem let_value_eq
modified theorem let_value_heq
deleted theorem mk_equivalence
deleted def non_contradictory
modified theorem not_of_eq_false
added theorem not_or_of_not
deleted theorem of_as_true
modified theorem of_heq_true
deleted theorem opt_param_eq
added theorem or_assoc'
added theorem or_comm'
added theorem or_false_iff
added theorem or_self_iff
added theorem or_true_iff
added theorem rec_subsingleton
deleted def reflexive
deleted def right_cancelative
modified theorem right_comm
deleted def right_commutative
deleted def right_distributive
deleted def right_identity
deleted def subrelation
deleted def symmetric
deleted def total
modified theorem trans_rel_left
modified theorem trans_rel_right
deleted def transitive
added theorem true_and_iff
added theorem true_iff_iff
added theorem true_or_iff
modified theorem unique_of_exists_unique
deleted def xor
added def bit0
added def bit1
modified theorem dec_em'
modified theorem em'
modified theorem xor_comm
modified theorem xor_false
modified theorem xor_self
modified theorem xor_true