Stream: Coq users

Topic: How to use nat in custom notations?


view this post on Zulip Daniel Hilst Selli (Feb 27 2022 at 00:04):

Hi folks,

I have this code

Inductive Add nat : Type :=
| id : nat -> Add nat
| add : Add nat -> nat -> Add nat.
Arguments id {_}.
Arguments add {_}.

Check id 1.
Check add (id 1) 1.
Check add (add (id 1) 1) 1.

Declare Custom Entry expr.
Notation "[ e ]" := e (e custom expr at level 2).
Notation "0" := (id 0) (in custom expr at level 0).
Notation "x + y" := (add x y) (in custom expr at level 2, left associativity).
Notation "x" := x (in custom expr at level 0, x ident).
Notation "{ x }" := x (in custom expr, x constr).

Unset Printing Notations.
Check [0 + {1} + {2}].
Set Printing Notations.

Fixpoint interp (s : Add nat) : nat :=
  match s with
  | id n => n
  | add s' n => interp s' + n
  end.

Eval simpl in  interp ([0 + {1} + {2} + {3}]).

I'm looking for a way to get rid of 0 in [0 + {1} + {2}] and also looking for a way to get rid of the braces, I mean, be able to do this [1 + 2 + 3] instead of [0 + {1} + {2} + {3]].


Last updated: Jan 28 2023 at 06:30 UTC