term elaborator for a term we know is wrong!

Stream: general

[Kim Morrison]

For the purpose of writing tutorials/documentation, it seems like it might be nice to have something like expectFailure% t, which checks that t can not be elaborated with the expected type, and then converts the type mismatch error into a warning.

Or, to #xy, how do people write "iterative" tutorials, where you show a few intermediate steps of constructing the desired term, without your file actually having errors?

[Eric Wieser]

Is one answer to use Verso's message-capturing support?

[Kim Morrison]

Hmm... it is a good point that I need to learn Verso asap. However for now I really prefer "hackable" tutorials, i.e. plain Lean files you can give to the consumers.

[Utensil Song]

I also needed something similar before, I wanted to demonstrate a weird parse issue that Lean will report "unexpected token '<-'; expected ':=' or '←'", but I guess your expectFailure% t won't cover this?

P.S. Is there a way to find all things (don't know what they are called either) that ends with %, I only see them on Zulip but haven't read about them anywhere else.

[Utensil Song]

I found a list here, and type_of% or ensure_type_of% might be able to be modified to suit your need?

[Anand Rao Tadipatri]

Verso supports code blocks with configuration option error:=true that display error messages in the rendered text without breaking the entire source file.

[Mario Carneiro]

Utensil Song said:

P.S. Is there a way to find all things (don't know what they are called either) that ends with %, I only see them on Zulip but haven't read about them anywhere else.

As I understand it, postfix % is supposed to mean "implementation detail macro", although I have seen people use it for general purpose macros as well

[Mario Carneiro]

I prefer the my_mac(e) syntax for general purpose macros

[Kyle Miller]

In mathlib we've been using % for term elaborators in general, not just things that are meant to be implementation details. In core the % was originally meant to indicate implementation details. Using % is partly a way to avoid reserving identifiers as keywords, and it's partly a way to say "this term is not just a normal application".

[Kyle Miller]

Where have you seen my_mac(e) syntax? The only cases I know of are syntax/qq/congr quotations. If you want, you can include syntax command items.