diff options
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 ----------------------------------------------------------------- |