search

dselsam / binport

A tool for building Lean4 .olean files from Lean3 export data
Apache License 2.0
10 stars 1 forks source link

Automatically construct `Trans` instances from relation manager exports #14

Open dselsam opened 3 years ago

dselsam commented 3 years ago

To be compatible with https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/microcalc/near/225283676