Zulip Chat Archive

Stream: Is there code for X?

Topic: does lean have assert?

Erika Su (Dec 23 2022 at 19:39):

I feel that a useful pattern for expressing constraints....

Reid Barton (Dec 23 2022 at 22:08):

Lean 4 does, at least

Erika Su (Dec 24 2022 at 12:36):

Reid Barton said:

Lean 4 does, at least

I am unable to find documenation about it, can you please give an example?

Adam Topaz (Dec 24 2022 at 14:28):

here is an example: https://github.com/leanprover/lean4/blob/85119ba9d1035e169a6d8718627314a096c19a29/tests/lean/run/parray1.lean

Last updated: Dec 20 2023 at 11:08 UTC