Lean4
/-- Makes a `match` expression corresponding to the application of `casesOn` like:
```lean
match (motive := motive) indices₁, indices₂, .., (val : type.{univs} params₁ params₂ ..) with
| _, _, .., ctor₁ fields₁₁ fields₁₂ .. => rhss ctor₁ [fields₁₁, fields₁₂, ..]
| _, _, .., ctor₂ fields₂₁ fields₂₂ .. => rhss ctor₂ [fields₂₁, fields₂₂, ..]
```
This is convenient to make a definition with equation lemmas. -/
def mkCasesOnMatch (type : Name) (levels : List Level) (params : List Expr) (motive : Expr) (indices : List Expr)
(val : Expr) (rhss : (ctor : Name) → (fields : List FVarId) → TermElabM Expr) : TermElabM Expr := do
let matcherName ← getDeclName? >>= (fun n? => Lean.mkAuxDeclName (.mkStr (n?.getD type) "match"))
let matchType ← generalizeTelescope (indices.concat val).toArray fun iargs => mkForallFVars iargs (motive.beta iargs)
let iinfo ← getConstInfoInduct type
let lhss ←
iinfo.ctors.mapM fun ctor => do
let cinfo ← getConstInfoCtor ctor
let catype ← instantiateForall (cinfo.type.instantiateLevelParams cinfo.levelParams levels) params.toArray
forallBoundedTelescope catype cinfo.numFields fun cargs _ => do
let fvarDecls ← cargs.toList.mapM fun carg => getFVarLocalDecl carg
let fieldPats := cargs.toList.map fun carg => Pattern.var carg.fvarId!
let patterns := [Pattern.ctor cinfo.name levels params fieldPats]
return
{ ref := .missing
fvarDecls
patterns }
let mres ←
Term.mkMatcher
{ matcherName
matchType
discrInfos := .replicate (indices.length + 1) { }
lhss }
mres.addMatcher
let rhss ←
lhss.mapM fun altLHS => do
let [.ctor ctor _ _ cpats] := altLHS.patterns |
unreachable!
withExistingLocalDecls altLHS.fvarDecls do
let fields := altLHS.fvarDecls.map LocalDecl.fvarId
let rhsBody ← rhss ctor fields
if cpats.isEmpty then
mkFunUnit rhsBody
else
mkLambdaFVars (fields.map Expr.fvar).toArray rhsBody
return mkAppN mres.matcher (motive :: indices ++ [val] ++ rhss).toArray
