Return syntax elems[0] ( elems[1] ... ( 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 + 1
    • f · · 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).

      Instances For