Specialized sorry for Type and Prop

Stream: lean4

[Tomas Skrivan]

Is there a specialized sorry for Type and Prop? I have sorry for Prop everywhere and a few for Type as well. Now I'm trying to compile and execute my library and I'm getting panic errors because I'm executing sorry. I would like to find all those Type sorry.

Or at least in the future use different sorry for Prop and Type to exactly see what breaks execution.

[Henrik Böving]

As far as I know sorry is basically just a frontend for https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#sorryAx so in theory it should be possible to split this into two axioms, one for Prop and one for Type u

[Kyle Miller]

(deleted)

[Tomas Skrivan]

Yeah I already inspected sorryAx a bit and sorry has custom elaborator that print the warning message. I was thinking about writing my own axiom like that purely for Prop and purely for Type. Then I got lazy, wondered if it already exists so I asked :)

[Gabriel Ebner]

so in theory it should be possible to split this into two axioms

Not really, you can also have this:

example (α : Sort u) : α := sorry

[Henrik Böving]

Well yes but it should be possible to have an additional sorryProp and sorryType right?

[Mac]

@Tomas Skrivan you could mark your new sorryType noncomputable so that definitions using it will error when compiling.

[Kyle Miller]

Lean spelunking question: where is sorry actually defined? I haven't been able to find it, or what turns it into sorryAx.

[Tomas Skrivan]

In emacs, go to definition on sorry takes you to BuiltNotation.lean and there elabSorry

[Kyle Miller]

Thanks. (I need to fix my go-to-definition for Lean 4; it works for most things, just not sorry apparently.)

https://github.com/leanprover/lean4/blob/9a24db4e86af9b39db7df3094c7aab05bd5c9a64/src/Lean/Elab/BuiltinNotation.lean#L157

[Tomas Skrivan]

(deleted)