Disable dot notation

Stream: new members

[Ranjit Jhala]

Hi all, is there a way to disable "dot notation". What I mean is, owing to my FP background I'd rather read reverse l instead of l.reverse and more importantly, I'd rather see node l x r instead of l.node x r, for the node case of a datatype defined as:

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α -> α -> Tree α -> Tree α
  deriving Repr

is there some way to get the "non dotted" representation?

thanks!

[Etienne Marion]

Is this what you want?

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α -> α -> Tree α -> Tree α
  deriving Repr

open Tree

variable (a b : Tree Nat)

#check node a 0 b

[Daniel Weber]

You can use

attribute [pp_nodot] Tree.node

to disable it for a specific function or

set_option pp.fieldNotation false

to disable it globally

[Ranjit Jhala]

Thanks @Daniel Weber !

[Ranjit Jhala]

@Etienne Marion -- not quite, I wanted the thing Daniel suggested, to just disable the fieldNotation. Thanks!

[Trevor Hyde]

I tried adding this option to my lakefile:
Screenshot 2025-01-17 at 12.30.50 PM.png
I then ran lake update and restarted my files, but I still see the dot notation.
Screenshot 2025-01-17 at 12.31.40 PM.png
Where have I gone wrong?