Topic: Shameless lean 4 request
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
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
Reid Barton (Nov 23 2018 at 01:18):
I thought there was something like this already.
Keeley Hoek (Nov 23 2018 at 01:21):
Praise be! weird name
Reid Barton (Nov 23 2018 at 01:22):
Last updated: May 17 2021 at 21:12 UTC