I have a value to compute that's really fast to get through hnf
but takes ages with any other reduction strategy (cbn/lazy/vm/native). Is there a trick to produce a proof of t = hnf t
accepted by the kernel just as fast? I can't think of any way to do it currently.
Does the order matter? ie maybe hnf t = t
is faster
or maybe some reduction strat commands
But we don't carry them to the kernel right?
Strategy
and Opaque/Transparent go in the oracle used by kernel conversion
If you ask me, it's a good thing that hnf is not part of the kernel.
Ah you mean an unfolding strategy, sorry I misunderstood
Pierre-Marie Pédrot said:
If you ask me, it's a good thing that hnf is not part of the kernel.
TCB-wise I understand, but its still a pity my tactic takes 3sec and Qed 1 min
You might hack your way around adding enough casts here and there...
Hmm, I found another way by changing the big proof term I got by an opaque thing.
Last updated: Oct 13 2024 at 01:02 UTC