Zulip Chat Archive

Stream: general

Topic: Shameless lean 4 request


view this post on Zulip Keeley Hoek (Nov 23 2018 at 01:17):

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.

view this post on Zulip Reid Barton (Nov 23 2018 at 01:18):

I thought there was something like this already. undefined_core?

view this post on Zulip Keeley Hoek (Nov 23 2018 at 01:21):

Praise be! weird name

view this post on Zulip Reid Barton (Nov 23 2018 at 01:22):

Haha, yes


Last updated: May 17 2021 at 21:12 UTC