Some general guidelines about src syntax, the core AST - FStarLang/FStar GitHub Wiki

• 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 inspect Tm_delayed nodes
• Build terms that have binders in them using Util.abs, Util.arrow, etc.
• Otherwise, see Subst.close* and Subst.open* to work with binders
• General rule: do not manipulate de Bruijn indices yourself

Add to this, as needed