def
Lean.Elab.WF.withFixedPrefix
{α : Type}
(fixedPrefix : Nat)
(preDefs : Array Lean.Elab.PreDefinition)
(k : Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α)
:
Equations
- Lean.Elab.WF.withFixedPrefix fixedPrefix preDefs k = Lean.Elab.WF.withFixedPrefix.go preDefs k fixedPrefix #[] (Array.map (fun x => x.value) preDefs)
def
Lean.Elab.WF.packMutual
(fixedPrefix : Nat)
(preDefsOriginal : Array Lean.Elab.PreDefinition)
(preDefs : Array Lean.Elab.PreDefinition)
:
If preDefs.size > 1, combine different functions in a single one using PSum.
This method assumes all preDefs have arity 1, and have already been processed using packDomain.
Here is a small example. Suppose the input is
f x :=
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => a
| Nat.succ n, a, b => (g ⟨x.1, n, a, b⟩).fst
g x :=
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => (a, b)
| Nat.succ n, a, b => (h ⟨x.1, n, a, b⟩, a)
h x =>
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => b
| Nat.succ n, a, b => f ⟨x.1, n, a, b⟩
this method produces the following pre definition
f._mutual x :=
PSum.casesOn x
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => a
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst
fun val =>
PSum.casesOn val
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => (a, b)
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a)
fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => b
| Nat.succ n, a, b =>
f._mutual (PSum.inl ⟨val.1, n, a, b⟩)
Remark: preDefsOriginal is used for error reporting, it contains the definitions before applying packDomain.
Equations
- One or more equations did not get rendered due to their size.