Hello, I would like to create a quoted term from two Gallina terms as inputs, unquote it, and assert it as a lemma. I know that the TemplateMonad can create proof obligations whenever the Lemma is not proved, thanks to the `tmLemma`

constructor. But I cannot make this typecheck because the monad cannot resolve the implicit arguments. Here is a minimal example:

```
From MetaCoq Require Import All.
From MetaCoq.Template Require Import utils.
Import MCMonadNotation.
Require Import List.
Import ListNotations.
Definition mkEq A t t' := tApp <% @eq %> [A; t ; t'].
Definition assert_equality {A : Type}
(t: A) (t': A) :=
tquote <- tmQuote t ;;
t'quote <- tmQuote t' ;;
A_quote <- tmQuote A ;;
let st := mkEq A_quote tquote t'quote in
st_unq <- tmUnquoteTyped Prop st;;
na <- tmFreshName "new_lemma";;
tmLemma na st_unq.
```

Do you know how I can do it? I use MetaCoq version 1.1-8.14. Thanks in advance !

The error message is misleading :) The problem is the return type of your function. What would you say it is?

(It depends on `t`

and `t'`

I think

the problem becomes more apparent when you write everything using `tmBind`

explicitly

```
Definition assert_equality {A : Type}
(t: A) (t': A) : TemplateMonad unit :=
tmBind (tquote <- tmQuote t ;;
t'quote <- tmQuote t' ;;
A_quote <- tmQuote A ;;
let st := mkEq A_quote tquote t'quote in
tmUnquoteTyped Prop st) (fun st_unq : Prop =>
na <- tmFreshName "new_lemma" ;;
_ <- tmLemma na st_unq;;
tmPrint "ok").
```

I easily get confused with monadic notations but I can see more clearly the problem. Thank you very much Yannick :)

Last updated: May 24 2024 at 21:01 UTC