-- | `later meta args` defers the invocation of `meta args`
\meta later

{- | `fails meta args` succeeds if and only if `meta args` fails

 - `fails {T} meta args` succeeds if and only if `meta args : T` fails

 -}
\meta fails

-- | `using (e_1, ... e_n) e` adds `e_1`, ... `e_n` to the context before checking `e`
\meta using

-- | `usingOnly (e_1, ... e_n) e` replaces the context with `e_1`, ... `e_n` before checking `e`
\meta usingOnly

-- | `hiding (x_1, ... x_n) e` hides local variables `x_1`, ... `x_n` from the context before checking `e`
\meta hiding

-- | `run { e_1, ... e_n }` is equivalent to `e_1 $ e_2 $ ... $ e_n`
\meta run

-- | `((f_1, ... f_n) at x) r` replaces variable `x` with `f_1 (... (f_n x) ...)` and runs `r` in the modified context
\meta \infix  at

-- | `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`.
\meta \infixr  in

{- | `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', 'name', and 'as'.
 - Parameter 'name' can be used to specify the name of the argument which can be used in types of subsequent arguments.
 - Parameter 'as' can be used to specify an \as-name that will be added to corresponding patterns in each clause.
 - 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)`.

 -}
\meta cases

{- | `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.

 -}
\meta mcases

{- | `unfold (f_1, ... f_n) e` unfolds functions/fields/variables `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`.

 -}
\meta unfold

-- | Unfolds \let expressions
\meta unfold_let

-- | Unfolds recursively top-level functions and fields
\meta unfolds

{- | `x <|> y` invokes `x` and if it fails, invokes `y`
 - Also, `(x <|> y) z_1 ... z_n` is equivalent to `x z_1 ... z_n <|> z_1 ... z_n`
 -}
\meta \infixr  <|>

-- | The same as {<|>}
\meta try

{- | Inserts data type arguments in constructor invocation.
 - If constructor `con` has 3 data type arguments, then `mkcon con args` is equivalent to `con {_} {_} {_} args`
 -}
\meta mkcon

{- | * `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.

 -}
\meta assumption

-- | `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,
\meta defaultImpl