Commit 2023-09-13 01:17 99672163

View on Github →

feat: nondeterminism monad, and use in backtrack (#3464)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MLList/Basic.lean

added def MLList.singleton

added def MLList.singletonM

Created Mathlib/Data/Nondet/Basic.lean

added def Nondet.filter

added def Nondet.filterMap

added def Nondet.firstM

added def Nondet.head

added def Nondet.map

added def Nondet.nil

added def Nondet.ofList

added def Nondet.ofListM

added def Nondet.ofOption

added def Nondet.ofOptionM

added def Nondet.singleton

added def Nondet.singletonM

added def Nondet.squash

added def Nondet.toList'

added def Nondet.toList

added def Nondet.toMLList'

added structure Nondet

Modified Mathlib/Tactic.lean

Renamed Mathlib/Tactic/Backtracking.lean to Mathlib/Tactic/Backtrack.lean

modified def Lean.MVarId.firstContinuation

Modified Mathlib/Tactic/GCongr/Core.lean

Modified Mathlib/Tactic/LibrarySearch.lean

modified def Mathlib.Tactic.LibrarySearch.sortResults

Modified Mathlib/Tactic/SolveByElim.lean

Created test/Nondet.lean

added def M

added def divisors

added def divisorsM

added def iotaM

added def record

added def x

added def y