diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index 680b1aa..99757a1 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -540,7 +540,8 @@ open Macro Comp in def elabData : CommandElab := fun stx => do let modifiers ← elabModifiers stx[0] let decl := stx[1] - let view ← dataSyntaxToView modifiers decl + /- Transforms binders into simple lambda types. -/ + let view ← dataSyntaxToView modifiers decl >>= preProcessCtors let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do let (nonRecView, _rho) ← makeNonRecursive view; diff --git a/Test/WithBindersInCtor.lean b/Test/WithBindersInCtor.lean index af4fa54..4b56fce 100644 --- a/Test/WithBindersInCtor.lean +++ b/Test/WithBindersInCtor.lean @@ -1,5 +1,13 @@ -import Qpf +import Qpf.Macro.Data -data QpfListWithBinder α +data QpfListWithBinder α + | cons (h : α) (tl : QpfListWithBinder α) | nil - | cons (hd : α) (tl : QpfListWithBinder α) \ No newline at end of file + +data Wrap α + | mk : α → Wrap α +data Wrap₂ α + | mk (a : α) : Wrap₂ α +data Wrap₃ α + | mk (a : α) +