Zulip Chat Archive
Stream: general
Topic: detecting sorry
Kevin Buzzard (Mar 02 2018 at 10:17):
I am assuming that the following should be easy, or at least possible.
Kevin Buzzard (Mar 02 2018 at 10:17):
I have a "definition" of an affine scheme in Lean
Kevin Buzzard (Mar 02 2018 at 10:17):
but it's not yet complete because it relies on a definition
Kevin Buzzard (Mar 02 2018 at 10:17):
which uses another definition
Kevin Buzzard (Mar 02 2018 at 10:18):
which uses another definition
Kevin Buzzard (Mar 02 2018 at 10:18):
which uses sorry
Patrick Massot (Mar 02 2018 at 10:18):
leanpkg build will tell you about this
Kevin Buzzard (Mar 02 2018 at 10:19):
I was expecting to be able to spot this in VS Code (or emacs)
Kevin Buzzard (Mar 02 2018 at 10:19):
but #print affine_scheme and #check affine_scheme don't seem to mention this
Gabriel Ebner (Mar 02 2018 at 10:23):
#print axioms affine_scheme should do the trick
Kevin Buzzard (Mar 02 2018 at 10:23):
Aah yes, thanks
Kevin Buzzard (Mar 02 2018 at 10:23):
I knew there was a way.
Kevin Buzzard (Mar 02 2018 at 10:23):
I used the powerful sorry axiom.
Kevin Buzzard (Mar 02 2018 at 10:24):
I wonder why they didn't make this part of ZFC.
Kevin Buzzard (Mar 02 2018 at 10:24):
<close topic>
Gabriel Ebner (Mar 02 2018 at 10:24):
IIRC it's a very well known large cardinal axiom.
Kevin Buzzard (Mar 05 2018 at 22:15):
Oh wait there's still something I don't understand
Kevin Buzzard (Mar 05 2018 at 22:15):
definition foo : ℕ → ℕ := sorry structure bar := (baz : ℕ → ℕ) (H : baz = foo) #print axioms bar
Kevin Buzzard (Mar 05 2018 at 22:15):
Claims no axioms
Kevin Buzzard (Mar 05 2018 at 22:16):
What I am hoping to find is either a method for detecting when my definition is finished
Kevin Buzzard (Mar 05 2018 at 22:16):
or a proof that this can't be done
Kevin Buzzard (Mar 05 2018 at 22:16):
but in my mind bar is not yet finished because it relies on unfinished foo
Mario Carneiro (Mar 06 2018 at 02:53):
#print axioms bar.mk
seems to work
Last updated: Dec 20 2023 at 11:08 UTC