Thomas Eckl (Sep 16 2020 at 11:32):
It is annoying that in the hott3-mode you cannot freely use
axiom because no conclusion is of type
Prop (in the sense of
Sort 0), so Lean3 will from time to time produce a
code generation failed, VM does not have code for ... message. For me, labelling facts as Theorems, Lemmas, Axioms and so on is a useful way to organise code and make it more readable.
I am wondering whether one can redefine their usage, maybe in the
hott attribute, in the following way: You are allowed to use them if the conclusion is of type
Prop in the HoTT sense, or if the type satisfies
is_prop (maybe relying on the class-instance mechanism). Is there anything which prevents you from doing it, like protected names etc? I did not do much meta-programming up to now, so don't want to start something which is hopeless anyway.
Here is also a related and more immediate problem: At one point in my code Lean complained that
VM does not have code for 'hott.trunc.is_trunc_trunc'. Now,
hott.trunc.is_trunc_trunc is declared as an
init.hit of the hott3 library. Shouldn't that be changed to a
constant, as it was in the Lean2 Hott library? Or is there a reason for calling it an
axiom now? If not, what's the best way to correct it? If I change it in my
init.hit file, do I have to recompile the hott3 library? And shall I raise an issue in GiTHub?
Sebastian Ullrich (Sep 16 2020 at 11:49):
constant are synonyms in Lean 3
Sebastian Ullrich (Sep 16 2020 at 11:50):
It's been a while, but can't you use
noncomputable theory (after the
imports) to ignore the code generation error?
Thomas Eckl (Sep 16 2020 at 15:06):
noncomputable theory at the top of the file nor
noncomputable in front of the
def removes the code generation error. Is that a problem? Or does the
noncomputable just prevent Lean to complain on (noncomputable) future uses of the definition?
Floris van Doorn (Sep 16 2020 at 18:31):
It is not easy to redefine what
def does vs
theorem. That is hard-coded in C++, so that would require a change in Lean itself. I agree it is annoying that you have to call everything
def instead of freely choosing
About the VM error: I don't know what causes that. Writing
hott_theory automatically marks that file as
noncomputable theory, and that should solve it. I remember that I've seen that error for incomplete definitions, or definitions with also some other error. If that was not the case, could you post a #mwe?
Thomas Eckl (Sep 17 2020 at 17:22):
When trying to minimise the code and erasing some
let ... in the VM error vanished. No explanation for this, but who cares ... Your hint helped, and I will live with
Last updated: May 09 2021 at 19:11 UTC