Flocq porting status

Stream: general

[Ching-Tsun Chou]

What is the status of porting Flocq to Lean? I see various allusions to such efforts in Zulip from time to time but can find no definite details. What is the status (or statuses) exactly?

[Henrik Böving]

It's not a port of Flocq but rather a somewhat original float mechanization but this is the most advanced one I'm aware of: https://github.com/opencompl/fp-lean