assert in lean?

Stream: lean4

[Siddharth Bhat]

Is there an equivalent to Haskell's assert in lean4? I could only find Lean.Meta.assert which does not do what I want. I want something along the lines of assert: Bool -> a -> a

[I know lean is meant to be total, does not have exceptions, and thus asking for such a feature is unsound. Regardless, it seems useful to have when debugging...]

[Henrik Böving]

If you just want to assert something python styleassert! does exist as a macro and is used a few times in the compiler.

[Henrik Böving]

Does work both in monadic and non monadic code.

[Siddharth Bhat]

Do you happen to know where it is elaborated? I can see that it is declared as a builtin for do notation, and as a term

[Henrik Böving]

docs4#Lean.Elab.Term.expandAssert seems to be the spot

[Leonardo de Moura]

@Henrik Böving Wow, everytime I look at the docs4 generated files they look nicer.

[Siddharth Bhat]

Nice, yes, thanks!

[Siddharth Bhat]

@Henrik Böving maybe I'm missing something, but it seems the source location for expandAssert is linked to elabPanic? (This is the location I get)

[Henrik Böving]

Leonardo de Moura said:

Henrik Böving Wow, everytime I look at the docs4 generated files they look nicer.

Thanks!

There is actually one rather major thing I'm getting wrong at the moment. E.g. https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#ReaderT is marked as noncomputable (and so are a lot of others) because of the way I check for computability (https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process.lean#L206-L211) as metnioned above this is partially taken from ll_infer_type.cpp, specifically the part that generates errors about noncompuatbility https://github.com/leanprover/lean4/blob/master/src/library/compiler/ll_infer_type.cpp#L182-L205 but its only does the check for the existence of a cstage2 name and not this little if statement adn the foor loop because I didnt exactly get what this is doing so all stuff that does not have a cstage representation such as definitions that are just types are marked as noncomputable, could you enlighten me on what's happening there? Or how to do a computability check from within Lean in general.

[Henrik Böving]

Siddharth Bhat said:

Henrik Böving maybe I'm missing something, but it seems the source location for expandAssert is linked to elabPanic? (This is the location I get)

The actual declaration is right below , the generated location does seem to be wrong for some reason indeed...

[Leonardo de Moura]

@Henrik Böving I am assuming you want to reflect back in the documentation the noncomputable annotations provided by users in the .lean files, correct?

[Henrik Böving]

Yes.

[Leonardo de Moura]

Cool. I will add an API for this.

[Henrik Böving]

\o/

[Henrik Böving]

I did look around for such an API and eventually just figured I'd try translating the cpp code that seems to be responsible for checking the error :sweat_smile:

[Henrik Böving]

Henrik Böving said:

Siddharth Bhat said:

Henrik Böving maybe I'm missing something, but it seems the source location for expandAssert is linked to elabPanic? (This is the location I get)

The actual declaration is right below , the generated location does seem to be wrong for some reason indeed...

The length of the slice certainly does match its just offset for some reason...

[Henrik Böving]

#eval show MetaM _ from do
  findDeclarationRanges? `Lean.Elab.Term.expandAssert

Lean is also very much convinced that this declaration is at line 137 to 143 so this is probably a bug in the declaration range implementation, I opened an issue here https://github.com/leanprover/lean4/issues/1021

[Leonardo de Moura]

Henrik Böving said:

\o/

https://github.com/leanprover/lean4/blob/373a64ee09678d03db5eb27457ec4c2ae909abea/tests/lean/isNoncomputable.lean

[Henrik Böving]

I'll add it after the nightly is out tomorrow!

[Henrik Böving]

docs4#ReaderT docs4#Classical.choose done!