| Erefinementdecl of name * name * exp * exp * is_static| Econstdecl of name * is_static * exp
For now, we store non-refinement variable declaration like let var : type = exp as trivially true refinement variable in Erefinementdecl, but for declaration without type annotation (like let var = exp), we are still storing it in Econstdecl.
We hope to finally use a pattern called Econstdecl (which has the same name as the original one but with some modifications on inner data structure) to store all variable declarations
jchen-cs
commented
2 years ago
| Erefinementdecl of name * name * exp * exp * is_static| Econstdecl of name * is_static * expFor now, we store non-refinement variable declaration like
let var : type = expas trivially true refinement variable inErefinementdecl, but for declaration without type annotation (likelet var = exp), we are still storing it inEconstdecl.We hope to finally use a pattern called
Econstdecl(which has the same name as the original one but with some modifications on inner data structure) to store all variable declarations