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).
Would a coercion from
Unfortunately no, I should have specified, but coercions are pretty much a no go in my case
But in a sense precisely: I'd like to format the printing like coercion seems to be doing it under the hood.
Last updated: Jan 29 2023 at 01:02 UTC