Zulip Chat Archive

Stream: general

Topic: detecting sorry


view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:17):

I am assuming that the following should be easy, or at least possible.

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:17):

I have a "definition" of an affine scheme in Lean

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:17):

but it's not yet complete because it relies on a definition

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:17):

which uses another definition

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:18):

which uses another definition

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:18):

which uses sorry

view this post on Zulip Patrick Massot (Mar 02 2018 at 10:18):

leanpkg build will tell you about this

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:19):

I was expecting to be able to spot this in VS Code (or emacs)

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:19):

but #print affine_scheme and #check affine_scheme don't seem to mention this

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 10:23):

#print axioms affine_scheme should do the trick

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:23):

Aah yes, thanks

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:23):

I knew there was a way.

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:23):

I used the powerful sorry axiom.

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:24):

I wonder why they didn't make this part of ZFC.

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:24):

<close topic>

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 10:24):

IIRC it's a very well known large cardinal axiom.

view this post on Zulip Kevin Buzzard (Mar 05 2018 at 22:15):

Oh wait there's still something I don't understand

view this post on Zulip Kevin Buzzard (Mar 05 2018 at 22:15):

definition foo : ℕ → ℕ := sorry

structure bar :=
(baz : ℕ → ℕ)
(H : baz = foo)

#print axioms bar

view this post on Zulip Kevin Buzzard (Mar 05 2018 at 22:15):

Claims no axioms

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 05 2018 at 22:16):

or a proof that this can't be done

view this post on Zulip Kevin Buzzard (Mar 05 2018 at 22:16):

but in my mind bar is not yet finished because it relies on unfinished foo

view this post on Zulip Mario Carneiro (Mar 06 2018 at 02:53):

#print axioms bar.mk

seems to work


Last updated: May 15 2021 at 00:39 UTC