Commit bfb8f04e authored by Gregory Malecha's avatar Gregory Malecha Committed by Robbert

notation for forall

parent ea934fb9
......@@ -190,6 +190,11 @@ embedded logics. *)
Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope.
(** Change [forall] into a notation in order to enable overloading. *)
Notation "'forall' x .. y , P" := (forall x, .. (forall y, P%type) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : type_scope.
(** * Equality *)
(** Introduce some Haskell style like notations. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment