Tomas Uribe comments

Repositories
Issues
Comments

Results 3 comments of


                                            Tomas Uribe

Handle variable attributes in the Foreign Interface, if possible

Thanks, will do. Is it still OK to make issues, or should I ask on Discourse first? For example, looking for how to construct a rational number using the (C)...

Modification to "Book" paragraph in Learning Lean 4 page

I believe that "How to prove it with Lean" still uses Lean 3?

Modification to "Book" paragraph in Learning Lean 4 page

Thanks, I was hastily judging by https://djvelleman.github.io/HTPIwL/IntroLean.html, which does not mention a version. (All such pages should ideally mention which version of Lean they refer to / were tested on,...