rfl using #eval

Stream: Is there code for X?

[Kenny Lau]

I know it's potentially unsafe, but is there a version of rfl that uses #eval instead of the kernel? (sorry if i'm mixing up some terms, they still feel like the same thing to me)

[Mario Carneiro]

by native_decide

[Kenny Lau]

what if the rfl is not decidable?

[Mario Carneiro]

then you won't be able to use #eval to prove it

[Kenny Lau]

:thinking:

[Kenny Lau]

but in the example it's an inductive wrapper around something eval-able

[Mario Carneiro]

the issue is that while #eval can interpret a lot of types, it still needs to read the result back into the lean world, and this is difficult in nontrivial cases because the interpreter lost all the typing information. So the kernel primitive that lets you do this is only able to work with reifying elements of Bool and Nat since it's easy to interpret an interpreted value in one of these types. So the way native_decide works is it turns any goal into a check that a bool is equal to true and then runs that in #eval