## 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

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

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.

<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


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: May 15 2021 at 00:39 UTC