\module Meta

Scope metas

Meta using, usingOnly, and hiding controls the scope.

using (e_1, … e_n) e adds e_1, … e_n to the context before checking e. using (e_1, … e_n) is sometimes used in other context-manipulating metas, that adds e_1, … e_n to the context it uses.
usingOnly (e_1, … e_n) e replaces the context with e_1, … e_n before checking e. usingOnly (e_1, … e_n) is sometimes used in other context-manipulating metas, that replaces the context is uses with e_1, … e_n.
hiding (e_1, … e_n) e hides local bindings e_1, … e_n from the context before checking e. hiding (e_1, … e_n) is sometimes used in other context-manipulating metas, that hides e_1, … e_n from the context it uses.

cases

cases args default works just like mcases args default, but does not search for \case expressions or definition invocations. Each argument has a set of parameters that can be configured. Parameters are specified after keyword ‘arg’ which is written after the argument. Available parameters are ‘addPath’ and ‘name’. The latter can be used to specify the name of the argument which can be used in types of subsequent arguments. The type of an argument is specified as either e : E or e arg parameters : E. The flag ‘addPath’ indicates that argument idp with type e = x should be added after the current one, where e is the current argument and x is its name. That is, cases (e arg addPath) is equivalent to cases (e arg (name = x), idp : e = x).

mcases

mcases {def} args default \with { … } finds all invocations of definition def in the expected type and generate a \case expression that matches arguments of those invocations. It matches only those arguments which are matched in def. If the explicit argument is omitted, then mcases searches for \case expressions instead of definition invocations. default is an optional argument which is used as a default result for missing clauses. The list of clauses after \with can be omitted if the default expression is specified. args is a comma-separated list of expressions (which can be omitted) that will be additionally matched in the resulting \case expressions. These arguments are written in the same syntax as arguments in cases. mcases also searches for occurrences of def in the types of these additional expressions. Parameters of found arguments can be specified in the second implicit argument. The syntax is similar to the syntax for arguments in cases, but the expression should be omitted. If the first implicit argument is _, it will be skipped. mcases {def_1, … def_n} searches for occurrences of definitions def_1, … def_n. mcases {def, i_1, … i_n} matches arguments only of i_1-th, … i_n-th occurrences of def. For example,

mcases {(def1,4),def2,(def3,1,2)} looks for the 4th occurrence of def1, all occurrences of def2, and the first and the second occurrence of def3.
mcases {(1,2),(def,1)} looks for the first and the second occurrence of a \case expression and the first occurrence of def.
mcases {(def1,2),(),def2} looks for the second occurrence of def1, all occurrences of \case expressions, and all occurrences of def2.
mcases {_} {arg addPath, arg (), arg addPath} looks for case expressions and adds a path argument after the first and the third matched expression.

unfold

unfold (f_1, … f_n) e unfolds functions f_1, … f_n in the expected type before type-checking of e and returns e itself. If the first argument is omitted, it unfold all fields. If the expected type is unknown, it unfolds these function in the result type of e.

unfold_let

unfold_let unfolds \let expressions

assumption

assumption searches for a proof in the context. It tries variables that are declared later first. assumption {n} returns the n-th variables from the context counting from the end. assumption {n} a1 … ak applies n-th variable from the context to arguments a1, … ak.

in

f in x is equivalent to \let r => f x \in r. Also, (f_1, … f_n) in x is equivalent to f_1 in … f_n in x. This meta is usually used with f being a meta such as rewrite, simplify, simp_coe, or unfold.

defaultImpl

defaultImpl C F E returns the default implementation of field F in class C applied to expression E. The third argument can be omitted, in which case either \this or _ will be used instead,