Shameless lean 4 request

Stream: general

[Keeley Hoek]

In Lean 4 could we please please please have something like Haskell's error, just a pure function which takes a string or format or something and otherwise acts just like sorry (but gives no sorry used warnings). Of course, it would have to be meta.

It would be a really big aid to metaprogramming, since right now every time I want to define a pure function used in a program which has some invalid arguments I have to make it fail silently for that invalid input, instead of returning a nice warning---or more likely from a practical perspective, make everything tactic for absolutely no reason and corrupt my entire program with tactic.

[Reid Barton]

I thought there was something like this already. undefined_core?

[Keeley Hoek]

Praise be! weird name

[Reid Barton]

Haha, yes