port of LoVe

Stream: lean4

[Matthew Ballard]

I've seen some passing mentions of porting Logical Verification to Lean 4. Who (if anyone) is working on this and what is the current status? Thanks.

[Alex J. Best]

I imagine @Jasmin Blanchette is working on this and may be able to give you an update.

[Matthew Ballard]

I saw @Jannis Limperg mention something also (if memory doesn't fail me).

[Jasmin Blanchette]

The status is that we're quite far -- almost completely done -- except that I was waiting for the definition of "abs" on rational numbers to appear and a few other things for Chapter 14. The rest would need a thorough reading pass to catch all the "list" vs. "List" etc.

[Jasmin Blanchette]

Why are you asking?

[Matthew Ballard]

Wonderful! I’m teaching an undergraduate course based on LoVe here and would vastly prefer Lean 4. I was wondering if there was something I could help beta test.

[Jasmin Blanchette]

Yes. Maybe the easiest is that I give you access to the repository where this all lives? If you give me your github user name, I could arrange that.

[Jasmin Blanchette]

Also, I might respond more quickly if you send me emails -- I'm not every day on the Lean chat. My address is jasmin.blanchette@gmail.com.

[Jasmin Blanchette]

It would be great if you could beta-test the material! I'm not sure when I'm going to teach the course again, due to a move.