Documentation

Like elabBinders, but also pass syntax node per binder. elabBinders(Ex) automatically adds binder info nodes for the produced fvars, but storing the syntax nodes might be necessary when later adding the same binders back to the local context so that info nodes can manually be added for the new fvars; see MutualDef for an example.

Elaborate the given binders (i.e., Syntax objects for simpleBinder <|> bracketedBinder), update the local context, set of local instances, reset instance chache (if needed), and then execute k with the updated context. The local context will only be included inside k.

For example, suppose you have binders [(a : α), (b : β a)], then the elaborator will create two new free variables a and b, push these to the context and pass to k #[a,b].

Same as elabBinder with a single binder.

The dependent arrow. (x : α) → β is equivalent to ∀ x : α, β, but we usually reserve the latter for propositions. Also written as Π x : α, β (the "Pi-type") in the literature.

Auxiliary function for expanding fun notation binders. Recall that fun parser is defined as

def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
leading_parser unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser

to allow notation such as fun (a, b) => a + b, where (a, b) should be treated as a pattern. The result is a pair (explicitBinders, newBody), where explicitBinders is syntax of the form

`(` ident `:` term `)`

which can be elaborated using elabBinders, and newBody is the updated body syntax. We update the body syntax when expanding the pattern notation. Example: fun (a, b) => a + b expands into fun _a_1 => match _a_1 with | (a, b) => a + b. See local function processAsPattern at expandFunBindersAux.

The resulting Bool is true if a pattern was found. We use it "mark" a macro expansion.

Expand matchAlts syntax into a full match-expression. Example | 0, true => alt_1 | i, _ => alt_2 expands into (for tactic == false) fun x_1 x_2 => match @x_1, @x_2 with | 0, true => alt_1 | i, _ => alt_2 and (for tactic == true) intro x_1; intro x_2; match @x_1, @x_2 with | 0, true => alt_1 | i, _ => alt_2

Remark: we add @ to make sure we don't consume implicit arguments, and to make the behavior consistent with fun. Example:

inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T

def makeT (f : forall {a : Type}, a -> a) : T :=
  mkT f

def makeT' : (forall {a : Type}, a -> a) -> T
| f => mkT f

The two definitions should be elaborated without errors and be equivalent.

Similar to expandMatchAltsIntoMatch, but supports an optional where clause.

Expand matchAltsWhereDecls into let rec + match-expression. Example ``` | 0, true => ... f 0 ... | i, _ => ... f i + g i ... where f x := g x + 1

  g : Nat → Nat
    | 0   => 1
    | x+1 => f x
```
expands into
```
fux x_1 x_2 =>
  let rec
    f x := g x + 1,
    g : Nat → Nat
      | 0   => 1
      | x+1 => f x
  match x_1, x_2 with
  | 0, true => ... f 0 ...
  | i, _    => ... f i + g i ...
```