A question on mrun - just to make sure I understood it correctly: mrun can be called with an argument which:

- has a return type of
`M.t <current goal type>`

- has a return type of
`tactic`

In the first case, if the tactic needs anything from the context, this must be passed explicitly to the term called with mrun as arguments. Also in the first case the tactic must solve the goal completely.

In the second case the tactic may inspect the context and may solve the goal partially by creating new goals.

This are the only ways in which mrun can be used.

Is this about correct?

In a `M. t A`

tactic you can still inspect the context (the list of hypotheses). You don't get explicitly the `goal`

, but that's the only difference in terms of inputs. When it comes to the solution, the difference is that the goals in the `M.t`

tactic are shelved, while in the `tactic`

one those returned in the list are unshelved.

I see. But I guess in case I have a `M.t A`

tactic where A is parametric, I get the parameters of A, so i can still be quite flexible in the goal type and inspect it via the parameters.

How do I inspect hypothesis with a `M.t A`

tactic?

Not sure what you mean. Say `t : forall {A}, M A`

and you need to prove `P`

. When you do `mrun t`

the following happens:

`A`

's meta-variable (created when typechecking`t`

) is unified with`P`

.`t`

is executed, say obtaining value`v`

.- The current goal is proved using
`v`

.

In every of these steps, the current context (that is, `P`

's dependencies) is part of the process. These can be obtain with the `M.hyps`

construct.

Not sure what you mean. Say

`t : forall {A}, M A`

and you need to prove`P`

. When you do`mrun t`

the following happens:

`A`

's meta-variable (created when typechecking`t`

) is unified with`P`

.`t`

is executed, say obtaining value`v`

.- The current goal is proved using
`v`

.

yes this is what I meant. As a response to your previous statement "You don't get explicitly the goal" I just wanted to say that one still can get complete information about the goal.

In every of these steps, the current context (that is,

`P`

's dependencies) is part of the process. These can be obtain with the`M.hyps`

construct.

Thanks - I somehow missed M.hyps.

Last updated: Feb 06 2023 at 06:29 UTC