Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
Require Export Basics.Utf8 Basics.Overture Basics.Iff.Require Export Basics.Utf8 Basics.Overture Basics.Iff.
(** * Just enough UTF8/Unicode for the Classes library to build, without depending on everything that HoTT.Utf8 depends on. *)
(* Logic *)
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) : type_scope.
Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) : type_scope.
Notation "x ∧ y" := (x /\ y) : type_scope.
Notation "x → y" := (x -> y) : type_scope.
Notation "x ↔ y" := (x <-> y) : type_scope.
(*Notation "¬ x" := (not x) : type_scope.*)
(*Notation "x ≠ y" := (x <> y) : type_scope.*)
(* Abstraction *)
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..).