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