Commit 2025-04-04 03:46 e0ec62bb

View on Github →

chore: split Data.Ordmap.Ordset (#23529) The constituent parts of the invariant have been pushed backwards to Data.Ordmap.Invariants. The bundled Valid predicate and Ordset itself remain in place.

Estimated changes

added theorem Ordnode.All.imp
added theorem Ordnode.Any.imp
added theorem Ordnode.Balanced.dual
added def Ordnode.Balanced
added theorem Ordnode.Bounded.dual
added theorem Ordnode.Bounded.mem_gt
added theorem Ordnode.Bounded.mem_lt
added theorem Ordnode.Bounded.of_gt
added theorem Ordnode.Bounded.of_lt
added theorem Ordnode.Bounded.to_lt
added theorem Ordnode.Bounded.to_nil
added theorem Ordnode.Bounded.to_sep
added theorem Ordnode.Bounded.weak
added def Ordnode.Bounded
added theorem Ordnode.Raised.dist_le
added theorem Ordnode.Raised.right
added def Ordnode.Raised
added theorem Ordnode.Sized.balance'
added theorem Ordnode.Sized.dual
added theorem Ordnode.Sized.dual_iff
added theorem Ordnode.Sized.eq_node'
added theorem Ordnode.Sized.node'
added theorem Ordnode.Sized.node3L
added theorem Ordnode.Sized.node3R
added theorem Ordnode.Sized.node4L
added theorem Ordnode.Sized.pos
added theorem Ordnode.Sized.rotateL
added theorem Ordnode.Sized.rotateR
added theorem Ordnode.Sized.size_eq
added def Ordnode.Sized
added theorem Ordnode.all_balance'
added theorem Ordnode.all_balanceL
added theorem Ordnode.all_balanceR
added theorem Ordnode.all_dual
added theorem Ordnode.all_iff_forall
added theorem Ordnode.all_node'
added theorem Ordnode.all_node3L
added theorem Ordnode.all_node3R
added theorem Ordnode.all_node4L
added theorem Ordnode.all_node4R
added theorem Ordnode.all_rotateL
added theorem Ordnode.all_rotateR
added theorem Ordnode.all_singleton
added theorem Ordnode.any_iff_exists
added theorem Ordnode.any_singleton
added def Ordnode.balance'
added theorem Ordnode.balancedSz_up
added theorem Ordnode.delta_lt_false
added theorem Ordnode.dual_balance'
added theorem Ordnode.dual_balanceL
added theorem Ordnode.dual_balanceR
added theorem Ordnode.dual_dual
added theorem Ordnode.dual_eraseMax
added theorem Ordnode.dual_eraseMin
added theorem Ordnode.dual_insert
added theorem Ordnode.dual_node'
added theorem Ordnode.dual_node3L
added theorem Ordnode.dual_node3R
added theorem Ordnode.dual_node4L
added theorem Ordnode.dual_node4R
added theorem Ordnode.dual_rotateL
added theorem Ordnode.dual_rotateR
added theorem Ordnode.emem_iff_all
added theorem Ordnode.equiv_iff
added theorem Ordnode.findMax'_all
added theorem Ordnode.findMax'_dual
added theorem Ordnode.findMax_dual
added theorem Ordnode.findMin'_all
added theorem Ordnode.findMin'_dual
added theorem Ordnode.findMin_dual
added theorem Ordnode.length_toList'
added theorem Ordnode.length_toList
added theorem Ordnode.merge_nil_left
added theorem Ordnode.merge_node
added def Ordnode.node3L
added theorem Ordnode.node3L_size
added def Ordnode.node3R
added theorem Ordnode.node3R_size
added def Ordnode.node4L
added theorem Ordnode.node4L_size
added def Ordnode.node4R
added theorem Ordnode.not_le_delta
added theorem Ordnode.raised_iff
added def Ordnode.realSize
added def Ordnode.rotateL
added theorem Ordnode.rotateL_nil
added theorem Ordnode.rotateL_node
added def Ordnode.rotateR
added theorem Ordnode.rotateR_nil
added theorem Ordnode.rotateR_node
added theorem Ordnode.size_balance'
added theorem Ordnode.size_balanceL
added theorem Ordnode.size_balanceR
added theorem Ordnode.size_dual
added theorem Ordnode.splitMax_eq
added theorem Ordnode.splitMin_eq
added theorem Ordnode.toList_nil
added theorem Ordnode.toList_node
deleted theorem Ordnode.All.imp
deleted theorem Ordnode.Any.imp
deleted theorem Ordnode.Balanced.dual
deleted def Ordnode.Balanced
deleted theorem Ordnode.BalancedSz.symm
deleted def Ordnode.BalancedSz
deleted theorem Ordnode.Bounded.dual
deleted theorem Ordnode.Bounded.dual_iff
deleted theorem Ordnode.Bounded.mem_gt
deleted theorem Ordnode.Bounded.mem_lt
deleted theorem Ordnode.Bounded.mono_left
deleted theorem Ordnode.Bounded.of_gt
deleted theorem Ordnode.Bounded.of_lt
deleted theorem Ordnode.Bounded.to_lt
deleted theorem Ordnode.Bounded.to_nil
deleted theorem Ordnode.Bounded.to_sep
deleted theorem Ordnode.Bounded.weak
deleted theorem Ordnode.Bounded.weak_left
deleted def Ordnode.Bounded
deleted theorem Ordnode.Raised.add_left
deleted theorem Ordnode.Raised.add_right
deleted theorem Ordnode.Raised.dist_le'
deleted theorem Ordnode.Raised.dist_le
deleted theorem Ordnode.Raised.right
deleted def Ordnode.Raised
deleted theorem Ordnode.Sized.balance'
deleted theorem Ordnode.Sized.dual
deleted theorem Ordnode.Sized.dual_iff
deleted theorem Ordnode.Sized.eq_node'
deleted theorem Ordnode.Sized.induction
deleted theorem Ordnode.Sized.node'
deleted theorem Ordnode.Sized.node3L
deleted theorem Ordnode.Sized.node3R
deleted theorem Ordnode.Sized.node4L
deleted theorem Ordnode.Sized.pos
deleted theorem Ordnode.Sized.rotateL
deleted theorem Ordnode.Sized.rotateR
deleted theorem Ordnode.Sized.size_eq
deleted def Ordnode.Sized
deleted theorem Ordnode.all_balance'
deleted theorem Ordnode.all_balanceL
deleted theorem Ordnode.all_balanceR
deleted theorem Ordnode.all_dual
deleted theorem Ordnode.all_iff_forall
deleted theorem Ordnode.all_node'
deleted theorem Ordnode.all_node3L
deleted theorem Ordnode.all_node3R
deleted theorem Ordnode.all_node4L
deleted theorem Ordnode.all_node4R
deleted theorem Ordnode.all_rotateL
deleted theorem Ordnode.all_rotateR
deleted theorem Ordnode.all_singleton
deleted theorem Ordnode.any_iff_exists
deleted theorem Ordnode.any_singleton
deleted def Ordnode.balance'
deleted def Ordnode.balanceL'
deleted def Ordnode.balanceR'
deleted theorem Ordnode.balance_sz_dual
deleted theorem Ordnode.balancedSz_down
deleted theorem Ordnode.balancedSz_up
deleted theorem Ordnode.balancedSz_zero
deleted theorem Ordnode.delta_lt_false
deleted theorem Ordnode.dual_balance'
deleted theorem Ordnode.dual_balanceL
deleted theorem Ordnode.dual_balanceR
deleted theorem Ordnode.dual_dual
deleted theorem Ordnode.dual_eraseMax
deleted theorem Ordnode.dual_eraseMin
deleted theorem Ordnode.dual_insert
deleted theorem Ordnode.dual_node'
deleted theorem Ordnode.dual_node3L
deleted theorem Ordnode.dual_node3R
deleted theorem Ordnode.dual_node4L
deleted theorem Ordnode.dual_node4R
deleted theorem Ordnode.dual_rotateL
deleted theorem Ordnode.dual_rotateR
deleted theorem Ordnode.emem_iff_all
deleted theorem Ordnode.equiv_iff
deleted theorem Ordnode.findMax'_all
deleted theorem Ordnode.findMax'_dual
deleted theorem Ordnode.findMax_dual
deleted theorem Ordnode.findMin'_all
deleted theorem Ordnode.findMin'_dual
deleted theorem Ordnode.findMin_dual
deleted theorem Ordnode.length_toList'
deleted theorem Ordnode.length_toList
deleted theorem Ordnode.merge_nil_left
deleted theorem Ordnode.merge_nil_right
deleted theorem Ordnode.merge_node
deleted def Ordnode.node3L
deleted theorem Ordnode.node3L_size
deleted def Ordnode.node3R
deleted theorem Ordnode.node3R_size
deleted def Ordnode.node4L
deleted theorem Ordnode.node4L_size
deleted def Ordnode.node4R
deleted theorem Ordnode.not_le_delta
deleted theorem Ordnode.pos_size_of_mem
deleted theorem Ordnode.raised_iff
deleted def Ordnode.realSize
deleted def Ordnode.rotateL
deleted theorem Ordnode.rotateL_nil
deleted theorem Ordnode.rotateL_node
deleted def Ordnode.rotateR
deleted theorem Ordnode.rotateR_nil
deleted theorem Ordnode.rotateR_node
deleted theorem Ordnode.size_balance'
deleted theorem Ordnode.size_balanceL
deleted theorem Ordnode.size_balanceR
deleted theorem Ordnode.size_dual
deleted theorem Ordnode.size_eq_realSize
deleted theorem Ordnode.splitMax_eq
deleted theorem Ordnode.splitMin_eq
deleted theorem Ordnode.toList_nil
deleted theorem Ordnode.toList_node