Commit 2023-05-01 11:02 0ed9c8d0

View on Github →

feat: port Mathlib.Data.Ordmap.Ordnode (#1455)

Estimated changes

added def Ordnode.All
added def Ordnode.Amem
added def Ordnode.Any
added def Ordnode.Emem
added def Ordnode.Equiv
added def Ordnode.alter
added def Ordnode.attach'
added def Ordnode.balance
added def Ordnode.balanceL
added def Ordnode.balanceR
added def Ordnode.delta
added def Ordnode.diff
added def Ordnode.disjoint
added def Ordnode.drop
added def Ordnode.dropAux
added def Ordnode.dual
added def Ordnode.empty
added def Ordnode.erase
added def Ordnode.eraseMax
added def Ordnode.eraseMin
added def Ordnode.filter
added def Ordnode.find
added def Ordnode.findGe
added def Ordnode.findGt
added def Ordnode.findLe
added def Ordnode.findLt
added def Ordnode.findMax'
added def Ordnode.findMax
added def Ordnode.findMin'
added def Ordnode.findMin
added def Ordnode.fold
added def Ordnode.foldl
added def Ordnode.foldr
added def Ordnode.glue
added def Ordnode.image
added def Ordnode.insert'
added def Ordnode.inter
added def Ordnode.isSubset
added def Ordnode.link
added def Ordnode.map
added def Ordnode.mem
added def Ordnode.merge
added def Ordnode.node'
added def Ordnode.nth
added def Ordnode.ofList'
added def Ordnode.ofList
added def Ordnode.pmap
added def Ordnode.powerset
added def Ordnode.ratio
added def Ordnode.repr
added def Ordnode.size
added def Ordnode.span
added def Ordnode.split3
added def Ordnode.split
added def Ordnode.splitAt
added def Ordnode.splitMax
added def Ordnode.splitMin
added def Ordnode.take
added def Ordnode.takeAux
added def Ordnode.toList
added def Ordnode.union
added inductive Ordnode