leanprover-community / lean4-samples

Code samples for Lean 4
Apache License 2.0
67 stars 22 forks source link

List Comprehension example of syntax extension. #10

Closed lovettchris closed 1 year ago

lovettchris commented 1 year ago

Many thanks to Kyle Miller who first posted this solution on Zulip, this sample then tests all the list comprehension features of Python now work in Lean.

Kha commented 1 year ago

There is a bit of inconsistent capitalization of "Lean" and "Python"

lovettchris commented 1 year ago

fixed, thanks.