From 870351e3a2f735678bd21d80083f0327b21fc588 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 8 Jan 2024 22:06:17 +0100 Subject: One/Unit --- example.txt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'example.txt') 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 -- cgit v1.2.3-70-g09d2