Mercurial > hg > Members > atton > agda > systemF

changeset 7:aac0c4fc941c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add comments
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 01 Apr 2014 15:31:29 +0900
parents e6a39088cb0a
children 1801268c523d
files systemF.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Tue Apr 01 15:24:12 2014 +0900
+++ b/systemF.agda	Tue Apr 01 15:31:29 2014 +0900
@@ -82,9 +82,10 @@
 ∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
 
 {-
-  proofs and types style
+  lemma-nabla on proofs and types
   (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
+  w[U/X][u/x^[U/X]]
 -}
 
-lemma-nabla : {X W U : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
+lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
 lemma-nabla = refl