-
Notifications
You must be signed in to change notification settings - Fork 232
Some general guidelines about src syntax, the core AST
Catalin Hritcu edited this page Oct 18, 2016
·
2 revisions
- See
syntax.fsi
for the core AST (term’ and term) - Using
Syntax.gen_bv/new_bv
to generate fresh names - Use
Subst.compress
before inspecting a term; never inspectTm_delayed
nodes - Build terms that have binders in them using
Util.abs
,Util.arrow
, etc. - Otherwise, see
Subst.close
* andSubst.open
* to work with binders - General rule: do not manipulate de Bruijn indices yourself
Add to this, as needed