Alias for sorry

Stream: new members

[Martin Dvořák]

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]

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]

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

[Kyle Miller]

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 :=
begin
  my_sorry,
end
-- declaration 'baz' uses sorry

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