Lean4
/-- `pairUp L R` takes to lists `L R : List Expr` as inputs.
It scans the elements of `L`, looking for a corresponding `DefEq` `Expr`ession in `R`.
If it finds one such element `d`, then it sets the element `d : R` aside, removing it from `R`, and
it continues with the matching on the remainder of `L` and on `R.erase d`.
At the end, it returns the sublist of `R` of the elements that were matched to some element of `R`,
in the order in which they appeared in `L`,
as well as the sublist of `L` of elements that were not matched, also in the order in which they
appeared in `L`.
Example:
```lean
#eval do
let L := [mkNatLit 0, (← mkFreshExprMVar (some (mkConst ``Nat))), mkNatLit 0] -- i.e. [0, _, 0]
let R := [mkNatLit 0, mkNatLit 0, mkNatLit 1] -- i.e. [0, 1]
dbg_trace f!"{(← pairUp L R)}"
/- output:
`([0, 0], [0])`
the output LHS list `[0, 0]` consists of the first `0` and the `MVarId`.
the output RHS list `[0]` corresponds to the last `0` in `L`.
-/
```
-/
def pairUp : List (Expr × Bool × Syntax) → List Expr → MetaM ((List (Expr × Bool)) × List (Expr × Bool × Syntax))
| (m :: ms), l => do
match ← l.findM? (isDefEq · m.1) with
| none =>
let (found, unfound) ← pairUp ms l;
return (found, m :: unfound)
| some d =>
let (found, unfound) ← pairUp ms (l.erase d)
return ((d, m.2.1) :: found, unfound)
| _, _ => return ([], [])
