Mercurial > hg > Members > atton > agda-proofs

comparison moggi/moggi.agda @ 3:36c9175d9adb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Migrate moggi from atton/agda/moggi (0:530373ccbcee)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 02 Nov 2014 09:41:29 +0900
parents
children
comparison
equal deleted inserted replaced
2:4c1a6ce23f9e 3:36c9175d9adb
1 module moggi where
2
3
4 postulate A : Set
5 postulate A1 : Set
6 postulate A2 : Set
7
8 postulate x : A
9 postulate e1 : A1
10 --postulate f : A1 -> A2
11
12 data _==_ : {A : Set} -> A -> A -> Set where
13 refl : {x : A} -> x == x
14 sym : {x y : A} -> x == y -> y == x
15 trans : {x y z : A} -> x == y -> y == z -> x == z
16 congr : {x y : A1} -> (f : A1 -> A2) -> x == y ->
17 f x == f y
18
19 record Term (A : Set) : Set where
20 field
21 type : A
22 var : A -> (A -> A)
23 f : A1 -> A2
24 eq : (g1 : A1 -> A2) -> (g2 : A1 -> A2) -> g1 == g2
25