Return syntax Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))
Instances For
Return some if succeeded expanding · notation occurring in
the given syntax. Otherwise, return none.
Examples:
· + 1=>fun _a_1 => _a_1 + 1f · · b=>fun _a_1 _a_2 => f _a_1 _a_2 b
Instances For
Auxiliary function for expanding the · notation.
The extra state Array Syntax contains the new binder names.
If stx is a ·, we create a fresh identifier, store in the
extra state, and return it. Otherwise, we just return stx.
Helper method for elaborating terms such as (.+.) where a constant name is expected.
This method is usually used to implement tactics that function names as arguments (e.g., simp).