Commit 2024-01-05 01:23 19557c78

View on Github →

chore: bump std4 dependency (#9426) This is quite a substantial bump as Nondet / backtrack / solve_by_elim have all moved to Std.

Estimated changes

deleted def MLList.singleton
deleted def MLList.singletonM
deleted def Nondet.filter
deleted def Nondet.filterMap
deleted def Nondet.firstM
deleted def Nondet.head
deleted def Nondet.map
deleted def Nondet.nil
deleted def Nondet.ofList
deleted def Nondet.ofListM
deleted def Nondet.ofOption
deleted def Nondet.ofOptionM
deleted def Nondet.singleton
deleted def Nondet.singletonM
deleted def Nondet.squash
deleted def Nondet.toList'
deleted def Nondet.toList
deleted def Nondet.toMLList'
deleted structure Nondet
added theorem Option.bind_eq_bind'
deleted theorem Option.bind_eq_bind
deleted theorem Option.bind_eq_none'
deleted def Lean.NameMap.filter
deleted def Lean.MVarId.note
deleted def Lean.SMap.foldM
deleted def Except.emoji
deleted def List.tryAllM
deleted def M
deleted def divisors
deleted def divisorsM
deleted def iotaM
deleted def record
deleted def x
deleted def y