diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2025-03-07 17:21:52 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2025-03-13 13:21:06 +0000 |
| commit | 1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d (patch) | |
| tree | f88834cd7b029343a1ad4a5969258e4022fdd00d /src/Inky/Term.idr | |
| parent | f5b75edd91389f0a45045b707abfa36c746e8d54 (diff) | |
Make `foldcase` syntactic sugar.
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 5 |
1 files changed, 5 insertions, 0 deletions
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 ----------------------------------------------------------------- |