importing without notations

Stream: new members

[Mike Shulman]

I have defined the following structure:

structure iso (X Y : Type) :=
  (to : X → Y)
  (fro : Y → X)
  (to_fro : ∀(y : Y), to (fro y) = y)
  (fro_to : ∀(x : X), fro (to x) = x)

This works fine, but when I add import tactic to the top of the file, suddenly on the second Iine I get the error invalid field, identifier expected. I assume that this means that tactic or some file it imports has declared to as part of some kind of notation, making it invalid for use as a field name. Can I import tactic without importing that notation, so that I don't have to rename to throughout my file? E.g. the equivalent of Agda import ... hiding?

[Adam Topaz]

Are you avoiding using docs#equiv ?

[Alex J. Best]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/reserved_notation.lean#L45 is the offending line btw

[Andrew Yang]

I don't think there is a way to hide imported notation.
You can use «to» instead (\f<< and \f>>) when they appear on its own, and after that iso.to (and f.to for f : iso X Y) should work without problems.

[Mike Shulman]

Andrew Yang said:

You can use «to» instead (\f<< and \f>>) when they appear on its own, and after that iso.to (and f.to for f : iso X Y) should work without problems.

Thanks! Where can I read more about what «...» means?

[Mike Shulman]

Adam Topaz said:

Are you avoiding using docs#equiv ?

Yes. (-:O

In general, prefer my students to see the definitions of the structures they're working with right there in the file, rather than having to look them up in a library. And up until now I've also been avoiding using mathlab entirely, for this and other reasons.

[Alex J. Best]

It's just a way of escaping names which allows you to put dots or spaces or all sorts of other weird things into your identifiers.
Searching "french double quotes" is the keyword and this is in the reference manual https://leanprover.github.io/reference/lexical_structure.html#identifiers, but probably most people learn about it on zulip