search

dselsam / binport

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

Make sure all standard Lean4 constructions are constructed #13

Closed dselsam closed 3 years ago

dselsam commented 3 years ago
dselsam commented 3 years ago

This issue is coupled with https://github.com/dselsam/mathport/issues/3 since some inductive declarations are accepted by lean4 but cause constructions to fail.

dselsam commented 3 years ago

This works now except for the invalid inductive types (see https://github.com/dselsam/mathport/issues/3)