From 8c7f0616d2968522dc8e6688944e5ac0a5644324 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sun, 29 Dec 2024 22:24:32 -0800
Subject: [PATCH] fix type constructor quantities for short data decls

---
 src/Lib/ProcessDecl.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 8c4622e..669e478 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -418,7 +418,7 @@ processDecl ns (Instance instfc ty decls) = do
 
 processDecl ns (ShortData fc lhs sigs) = do
   (nm,args) <- getArgs lhs []
-  let ty = foldr (\ (fc,n), a => (RPi fc (BI fc n Explicit Many) (RU fc) a)) (RU fc) args
+  let ty = foldr (\ (fc,n), a => (RPi fc (BI fc n Explicit Zero) (RU fc) a)) (RU fc) args
   cons <- traverse (mkDecl args []) sigs
   let dataDecl = Data fc nm ty cons
   putStrLn "SHORTDATA"