If I have a goal of type nat
, and I want to derive through typeclass resolution an instance of ThisNat n
where ThisNat
is a class and n
a concrete nat, then use n
to prove the goal.
Is there a way to do that using Ltac so that the resulting proof term is exactly n
, without any trace of the type class resolution or trace of ThisNat
?
Class Foo (n : nat).
Instance xxx : Foo 3. Defined.
Definition ooF n (_ : Foo n) := n.
Goal nat.
let solution := eval cbv in (ooF _ _) in exact solution.
Show Proof.
Right. I guess I wanted to avoid ooF
appearing in the proof term. But now I'm not sure it's very important
Ah wait nvm, didn't see the second part
thanks!
Last updated: Oct 13 2024 at 01:02 UTC