Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. 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.
Reserved Notation"'∀' x .. y , P"
(at level200, x binder, y binder, right associativity).Reserved Notation"'∃' x .. y , P"
(at level200, x binder, y binder, right associativity).
Identifier 'λ' nowakeyword
Reserved Notation"x ∧ y" (at level80, right associativity).Reserved Notation"x → y" (at level99, y at level200, right associativity).Reserved Notation"x ↔ y" (at level95, no associativity).(*Notation "¬ x" (at level 75, right associativity).*)(*Notation "x ≠ y" (at level 70).*)Reserved Infix"∩" (at level20).Reserved Infix"⋅" (at level20).Reserved Infix"∙" (at level20).Reserved Infix"∘" (at level40, left associativity).Reserved Infix"∘ˡ" (at level40, left associativity).Reserved Infix"∘ʳ" (at level40, left associativity).Reserved Infix"⊣" (at level60, right associativity).Reserved Infix"≅" (at level70, no associativity).
Identifier 'ᵒᵖ' now a keyword
Reserved Notation"A × B" (at level40, left associativity).Reserved Notation"a ≤ b" (at level70, no associativity).Reserved Notation"A ≃ B" (at level85).Reserved Notation"a ⇓ 'CAT'" (at level40, left associativity).Reserved Notation"a ⇑ 'CAT'" (at level40, left associativity).Reserved Notation"a ≤_{ x } b" (at level70, no associativity).Reserved Notation"C ↓ a" (at level70, no associativity).
Identifier 'CAT' now a keyword
Reserved Notation"'CAT' ⇑ a" (at level40, left associativity).Reserved Notation"C 'ᵒᵖ'" (at level3).Reserved Notation"C → D" (at level99, D at level200, right associativity).Reserved Notation"f '⁻¹'" (at level3, format"f '⁻¹'").(* Reserved Notation "f ×ᴱ g" (at level 40, no associativity). *)(* Reserved Notation "f *ᴱ g" (at level 40, no associativity). *)Reserved Notation"f +ᴱ g" (at level50, left associativity).Reserved Notation"F ₁ m" (at level10, no associativity).Reserved Notation"F ₀ x" (at level10, no associativity).Reserved Notation"g ∘ f" (at level40, left associativity).Reserved Notation"g ∘ᴱ f" (at level40, left associativity).Reserved Notation"m ⁻¹" (at level3, format"m '⁻¹'").Reserved Notation"m ≤ n" (at level70, no associativity).Reserved Notation"p '⁻¹'" (at level3, format"p '⁻¹'").Reserved Notation"p • q" (at level20).Reserved Notation"p •' q" (at level21, left associativity, format"'[v' p '/' '•'' q ']'").Reserved Notation"x ₁" (at level3).Reserved Notation"x ₂" (at level3).Reserved Notation"¬ x" (at level35, right associativity).Reserved Notation"x ⇓ F" (at level40, left associativity).Reserved Notation"x ⇑ F" (at level40, left associativity).Reserved Notation"x ∈ v" (at level30).Reserved Notation"x ⊆ y" (at level30).Reserved Notation"x ≠ y" (at level70).Reserved Notation"x ⇸ y" (at level99, right associativity, y at level200).Reserved Notation"x ↠ y" (at level99, right associativity, y at level200).Reserved Notation"x ↪ y" (at level99, right associativity, y at level200).Reserved Notation"A ⊗ B" (at level45, left associativity).(* Reserved Notation "∀ x .. y , P" (at level 200, x binder, y binder, right associativity). *)Reserved Notation"x ∨ y" (at level85, right associativity).(* Reserved Notation "x ⊔ y" (at level 85, right associativity). *)Reserved Infix"≶" (at level70, no associativity).Reserved Infix"⊓" (at level50, no associativity).Reserved Infix"⊔" (at level50, no associativity).Reserved Infix"∸" (at level50, left associativity).Reserved Notation"x ≤ y ≤ z" (at level70, y at next level).Reserved Notation"x ≤ y < z" (at level70, y at next level).Reserved Notation"x < y ≤ z" (at level70, y at next level).Reserved Notation"'π'" (at level0).