-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathworkinExamples.txt
More file actions
8 lines (8 loc) · 826 Bytes
/
workinExamples.txt
File metadata and controls
8 lines (8 loc) · 826 Bytes
1
2
3
4
5
6
7
8
p "data bool : Set where true | false"
p "data nat : Set where zero | suc ( n : nat ) "
p "caseBool ( x : Set ) ( y z : x ) : bool -> Set = split false -> y || true -> z"
p "indBool ( x : bool -> Set ) ( y : x ( false ) ) ( z : x ( true ) ) : ( b : bool ) -> x ( b ) = split false -> y || true -> z"
p "funExt ( a : Set ) ( b : a -> Set ) ( f g : ( x : a ) -> b ( x ) ) ( p : ( x : a ) -> ( b ( x ) ) ( f ( x ) ) == ( g ( x ) ) ) : ( ( y : a ) -> b ( y ) ) ( f ) == ( g ) = undefined"
p "foo ( b : bool ) : bool = b"
p "indBool ( x : bool -> Set ) ( y : x false ) ( z : x true ) : ( b : bool ) -> x b = split false -> y || true -> z"
p "funExt ( a : Set ) ( b : a -> Set ) ( f g : ( x : a ) -> b x ) ( p : ( x : a ) -> ( b x ) ( f x ) == ( g x ) ) : ( ( y : a ) -> b y ) f == g = undefined"