From 1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 7 Mar 2025 17:21:52 +0000
Subject: Rewrite for flap v2.0.0.

Make `foldcase` syntactic sugar.
---
 src/Inky/Term.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Inky/Term.idr')

diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 0f05f59..3c13580 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -95,6 +95,10 @@ data Term where
   Str :
     (meta : m) -> String ->
     Term (Sugar qtCtx) m tyCtx tmCtx
+  FoldCase :
+    (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Row (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x)) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
 
 %name Term e, f, t, u
 
@@ -122,6 +126,7 @@ export
 (List meta _).meta = meta
 (Cons meta _ _).meta = meta
 (Str meta _).meta = meta
+(FoldCase meta _ _).meta = meta
 
 --------------------------------------------------------------------------------
 -- Well Formed -----------------------------------------------------------------
-- 
cgit v1.2.3