diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-01-08 22:06:17 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-01-08 22:06:17 +0100 |
| commit | 870351e3a2f735678bd21d80083f0327b21fc588 (patch) | |
| tree | 92bf0fbd996b7c6713092e783b4fa7319c620840 /example.txt | |
| parent | ae603f2423e967c55dfd31b0dec26d19584aa322 (diff) | |
One/Unit
Diffstat (limited to 'example.txt')
| -rw-r--r-- | example.txt | 7 |
1 files changed, 5 insertions, 2 deletions
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 |