projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
53d4f1c
)
eliminate ext_tree_{left,right} keywords
author
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 14 Mar 2011 23:50:27 +0000
(16:50 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 14 Mar 2011 23:50:27 +0000
(16:50 -0700)
src/HaskProof.v
patch
|
blob
|
history
diff --git
a/src/HaskProof.v
b/src/HaskProof.v
index
7ae3462
..
efb9220
100644
(file)
--- a/
src/HaskProof.v
+++ b/
src/HaskProof.v
@@
-40,8
+40,8
@@
Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
Tree ??(LeveledHaskType Γ ★) ->
UJudg Γ Δ.
Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
Tree ??(LeveledHaskType Γ ★) ->
UJudg Γ Δ.
Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
- Notation "'ext_tree_left'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t) s end).
- Notation "'ext_tree_right'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end).
+ Definition ext_tree_left {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
+ Definition ext_tree_right {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
(* we can turn a UJudg into a Judg by simply internalizing the index *)
Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
(* we can turn a UJudg into a Judg by simply internalizing the index *)
Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=