Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (* in case "Require Export Utf8." doesn't work*)
- Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
- (at level 200, x binder, y binder, right associativity) : type_scope.
- Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
- (at level 200, x binder, y binder, right associativity) : type_scope.
- Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
- Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
- Notation "x → y" := (x -> y)
- (at level 90, y at level 200, right associativity): type_scope.
- Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope.
- Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope.
- Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
- (* Abstraction *)
- Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
- (at level 200, x binder, y binder, right associativity).
- Notation "x ≤ y" := (le x y) (at level 70, no associativity).
- Notation "x ≥ y" := (ge x y) (at level 70, no associativity).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement