feat: Fix binder issue

alexkeizer · Jun 24, 2024 · 8ef357b · 8ef357b
1 parent 9ae743a
commit 8ef357b
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 4 deletions.
diff --git 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
@@ -1,5 +1,13 @@
-import Qpf
+import Qpf.Macro.Data
 
-data QpfListWithBinder α 
+data QpfListWithBinder α
+  | cons (h : α) (tl : QpfListWithBinder α)
   | nil
-  | cons (hd : α) (tl : QpfListWithBinder α)
+
+data Wrap α
+  | mk : α → Wrap α
+data Wrap₂ α
+  | mk (a : α) : Wrap₂ α
+data Wrap₃ α
+  | mk (a : α)
+