diff options
| -rw-r--r-- | app/Main.hs | 2 | ||||
| -rw-r--r-- | example.txt | 7 |
2 files changed, 7 insertions, 2 deletions
diff --git a/app/Main.hs b/app/Main.hs index f8b586a..4c0014e 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -18,6 +18,8 @@ main = do let env0 = Map.fromList [("Level", Nothing :| TLevelUniv) + ,("One", Nothing :| TSet TIZero) + ,("Unit", Nothing :| TOne) ,("lzero", Nothing :| TLevel) ,("lsuc", Nothing :| TPi "x" TLevel TLevel)] diff --git a/example.txt b/example.txt index 1d96c5f..29ab618 100644 --- a/example.txt +++ b/example.txt @@ -1,2 +1,5 @@ -foo : (l : Level) -> (a : Set l) -> (x : a) -> a -foo = \(l : Level) -> \(a : Set l) -> \(x : a) -> x +id : (l : Level) -> (a : Set l) -> (x : a) -> a +id = \(l : Level) -> \(a : Set l) -> \(x : a) -> x + +unitfoo : (_ : One) -> One +unitfoo = \(Unit : One) -> Unit |