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:
4ec2860
)
note to self in HaskWeak
author
Adam Megacz
<megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:52:54 +0000
(20:52 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:52:54 +0000
(20:52 -0700)
src/HaskWeak.v
patch
|
blob
|
history
diff --git
a/src/HaskWeak.v
b/src/HaskWeak.v
index
85f5b24
..
22f0e60
100644
(file)
--- a/
src/HaskWeak.v
+++ b/
src/HaskWeak.v
@@
-20,6
+20,8
@@
Inductive WeakAltCon :=
Inductive WeakExpr :=
| WEVar : WeakExprVar -> WeakExpr
| WELit : HaskLiteral -> WeakExpr
Inductive WeakExpr :=
| WEVar : WeakExprVar -> WeakExpr
| WELit : HaskLiteral -> WeakExpr
+
+(* TO DO: add a WEWhere and use the source location to detect which one the user used *)
| WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
| WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
| WECast : WeakExpr -> WeakCoercion -> WeakExpr
| WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
| WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
| WECast : WeakExpr -> WeakCoercion -> WeakExpr