formatting.v

Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@  T1  }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
  (and T1 (and T2 .. (and Tn True)..))
  (* (format "'[v' {@  '[' T1 ']'  ;  '//' T2  ;  '//' ..  ;  '//' Tn  } ']'") *)
   : dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.
Check {@ True ; True -> False ; False } % dms.


Inductive ty := | TTop | TNat | TAnd (T1 T2 : ty).
Bind Scope ty_scope with ty.

Notation "⊤" := TTop : ty_scope.
Notation " {@ T1 } " := ( TAnd T1 TTop ) (format "{@  T1  }"): ty_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
  (TAnd T1 (TAnd T2 .. (TAnd Tn TTop)..))
  (format "'[v' {@  '[' T1 ']'  ;  '//' T2  ;  '//' ..  ;  '//' Tn  } ']'") : ty_scope.
Open Scope ty_scope.
Close Scope ty_scope.
Delimit Scope ty_scope with ty.
Check {@ TNat ; TNat ; TNat } % ty.
Check {@ TN ; True -> False ; False } % ty.
(* Format for second notation is ignored.
{@⊤; ⊤ -> False; False}%dms
	 : Prop
{@TNat; TNat; TNat}%ty
	 : ty
*)