Zulip Chat Archive

Stream: new members

Topic: Alias for sorry

Martin Dvořák (May 05 2022 at 05:26):

Is it possible to create alias for sorry so that, when I call #print axioms it will list all versions (all different names) of sorry that are (transitively) referenced by the given theorem?

Reid Barton (May 05 2022 at 10:23):

You can add axioms. As a degenerate case you could add axiom sorry2 {a : Sort*} : a, sorry3 ... but probably a more sensible thing to do is to turn the lemma you haven't proven yet into an axiom of the same type.

Reid Barton (May 05 2022 at 10:24):

Note that sorry itself is a bit special, e.g., it is a tactic too

Kyle Miller (May 05 2022 at 14:58):

sorry is also noisy -- as far as I know you can't make new axioms cause warnings.

Here's a hack I thought of to let you create a custom sorry that is both noisy (it says "uses sorry") and shows up in the axioms list.

constant my_sorry_reason {α : Sort*} : α  α

meta def tactic.interactive.my_sorry : tactic unit := `[exact my_sorry_reason sorry]

lemma baz (P Q : Prop) : P  Q :=
-- declaration 'baz' uses sorry

#print axioms baz
-- my_sorry_reason
-- [sorry]

Last updated: Dec 20 2023 at 11:08 UTC