search

dselsam / binport

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

Miscellaneous mismatches: dite, fin, unsigned, char, string, array, control structures, ... #11

Closed dselsam closed 3 years ago

dselsam commented 3 years ago

There are many things that might be nice to align that cannot be aligned naively.

  1. dite/ite: arguments are in different order
  2. fin: a def in lean3, structure in lean4
  3. unsigned vs UInt32: defined to be fin in lean3, structure containing a fin in lean4
  4. char vs Char: build on fin and unsigned
  5. string: builds on char
  6. has_seq_left vs SeqLeft: other arg must now be PUnit; this prevents auto-aligning e.g. monad
  7. array: length-indexed in lean3, not in lean4
dselsam commented 3 years ago

This issue has been split into multiple concrete ones.