Stream: Coq users

Topic: Notation: hiding unary constructor without parentheses

Yannick Zakowski (Oct 12 2020 at 16:30):

Is there a way to do something similar to the following and have the printer display Add 0 1 rather than Add (0) (1) by any chance?

Inductive foo: Type :=
        | Int (n : nat)
        | Add (m n : foo).
Notation "x" := (Int x) (only printing).
Check Add (Int 0) (Int 1).

Yao Li (Oct 12 2020 at 17:01):

Would a coercion from nat to foo work?

Yannick Zakowski (Oct 12 2020 at 17:04):

Unfortunately no, I should have specified, but coercions are pretty much a no go in my case

Yannick Zakowski (Oct 12 2020 at 17:06):

But in a sense precisely: I'd like to format the printing like coercion seems to be doing it under the hood.

Last updated: Apr 19 2024 at 21:01 UTC