diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-20 15:31:25 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-20 15:31:25 +0000 |
| commit | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (patch) | |
| tree | 32214f9e93eecbb6b1cc4aea12af1eba93f19ab7 /src/Inky/Term.idr | |
| parent | 3f72d28b7b348d441dde0e66e848ed4d7c16f5ba (diff) | |
Improve syntactic sugar.
Sugar makes programs nicer to write.
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 54ac9fe..8fd15aa 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -548,40 +548,3 @@ Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where uninhabited (ChecksNS Case) impossible uninhabited (ChecksNS Roll) impossible uninhabited (ChecksNS Fold) impossible - --- Sugar ----------------------------------------------------------------------- - -public export -CheckLit : m -> Nat -> Term mode m tyCtx tmCtx -CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<]) -CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n) - -public export -Lit : m -> Nat -> Term mode m tyCtx tmCtx -Lit meta n = Annot meta (CheckLit meta n) TNat - -public export -Suc : m -> Term mode m tyCtx tmCtx -Suc meta = - Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x")))) - (TArrow TNat TNat) - -export -isCheckLit : Term mode m tyCtx tmCtx -> Maybe Nat -isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0 -isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t -isCheckLit _ = Nothing - -export -isLit : Term mode m tyCtx tmCtx -> Maybe Nat -isLit (Annot _ t a) = - if (alpha {ctx2 = [<]} a TNat).does - then isCheckLit t - else Nothing -isLit _ = Nothing - -export -isSuc : Term mode m tyCtx tmCtx -> Bool -isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) = - does (alpha {ctx2 = [<]} a (TArrow TNat TNat)) -isSuc _ = False |