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: Jun 16 2024 at 01:42 UTC