assert! with a custom message?

Stream: lean4

[Chris Lovett]

anyone know off hand if I can custom ize the message reported by assert! in my lean unit tests? I want to do something like this: assert! ok; s!"the results are not as expected: {results}". I assume this is the implementation, but how would I modify this to allow a second argument to customize the message?

[Mario Carneiro]

That syntax is already taken by do notation, but you could do assert! cond | msg, which is what we are using in mathport

[Mario Carneiro]

There are two parts to each piece of syntax: the syntax and the elab/macro. For builtin syntax the syntax part is a bit verbose and found mostly in the Lean/Parser/Term.lean, Lean/Parser/Tactic.lean, Lean/Parser/Command.lean files

[Mario Carneiro]

what you found is the macro for assert

[Mario Carneiro]

You can get from the macro to the syntax by clicking on the name in the attribute, in this case @[builtinMacro Lean.Parser.Term.assert]