Mercurial > hg > Members > atton > agda > systemF

comparison systemF.agda @ 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
comparison
equal deleted inserted replaced
6:e6a39088cb0a 7:aac0c4fc941c
80 80
81 ∇_,_,_ : {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W 81 ∇_,_,_ : {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W
82 ∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w) 82 ∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
83 83
84 {- 84 {-
85 proofs and types style 85 lemma-nabla on proofs and types
86 (∇ X , x , w ) ⟨ U , u ⟩ ≡ w 86 (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
87 w[U/X][u/x^[U/X]]
87 -} 88 -}
88 89
89 lemma-nabla : {X W U : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w 90 lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
90 lemma-nabla = refl 91 lemma-nabla = refl