search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
41 stars 15 forks source link

fancy open/export options #4

Open digama0 opened 3 years ago

digama0 commented 3 years ago 
open foo as bar (a b c) hiding d e renaming f->g

Lean 4 supports the (...) explicits, hiding and renaming each individually, but not in conjunction, and the as bar part is not supported at all. This is a relatively rare feature but we might run into it.

Lean 3 also supports export with the same syntax, while lean 4 has a much more restricted export grammar. But this is only used a small handful of times so it is probably not a concern.

kim-em commented 3 years ago

mathlib barely uses open ... as ...: only in the continued fractions development, and it's pretty easy to remove: https://github.com/leanprover-community/mathlib/pull/9847