Lean4
/-- `Stained.toFMVarId mv lctx st` takes a metavariable `mv`, a local context `lctx` and
a `Stained` `st` and returns the array of pairs `(FVarId, mv)`s that `lctx` assigns to `st`
(the second component is always `mv`):
* if `st` "is" a `Name`, returns the singleton of the `FVarId` with the name carried by `st`;
* if `st` is `.goal`, returns the singleton `#[default]`;
* if `st` is `.wildcard`, returns the array of all the `FVarId`s in `lctx` with also `default`
(to keep track of the `goal`).
-/
def toFMVarId (mv : MVarId) (lctx : LocalContext) : Stained → Array (FVarId × MVarId)
| name n =>
match lctx.findFromUserName? n with
| none => #[]
| some decl => #[(decl.fvarId, mv)]
| goal => #[(default, mv)]
| wildcard => (lctx.getFVarIds.push default).map (·, mv)
