Mercurial > hg > Members > kono > Proof > category

diff record-ex.agda @ 315:0d7fa6fc5979

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
System T and System F
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Mar 2014 10:15:54 +0900
parents d6a6dd305da2
children
line wrap: on
line diff
--- a/record-ex.agda	Mon Jan 06 17:18:13 2014 +0900
+++ b/record-ex.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -35,6 +35,12 @@
 ya : A
 ya = and1 z
 
+lemma1 : A ∧ B → A
+lemma1 a =  and1 a
+
+lemma2 : A → B → A ∧ B 
+lemma2 a b =  record { and1 = a ; and2 = b }
+
 open  import  Relation.Binary.PropositionalEquality
 
 data Nat : Set where