diff options
Diffstat (limited to 'src/Term')
| -rw-r--r-- | src/Term/Semantics.idr | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr index 2e61040..dd76f62 100644 --- a/src/Term/Semantics.idr +++ b/src/Term/Semantics.idr @@ -10,6 +10,7 @@ TypeOf : Ty -> Type TypeOf N = Nat TypeOf (ty ~> ty') = TypeOf ty -> TypeOf ty' +public export rec : Nat -> a -> (a -> a) -> a rec 0 x f = x rec (S k) x f = f (rec k x f) @@ -66,3 +67,8 @@ fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do export sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty sem t = runIdentity (sem' t) + +export +arb : (ty : Ty) -> TypeOf ty +arb N = 0 +arb (ty ~> ty') = const (arb ty') |