search

dselsam / binport

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

Alignment not carrying over to namespaces #6

Open dselsam opened 3 years ago

dselsam commented 3 years ago

Currently, when we align e.g. list -> List, we do not change the list namespace to List, so dot-notation fails:

import Lean3Lib.init.data.list.basic
open Mathlib

#check list.nth ([2, 4] : List Nat) 1 -- succeeds
#check ([2, 4] : List Nat).nth 1 -- fails

This is not completely straightforward to fix since there may be clashing names.