1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation describing some of the fixity choices
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
-- There is no actual code in here, just design note.
module README.Design.Fixity where
-- binary relations of all kinds are infix 4
-- multiplication-like: infixl 7 _*_
-- addition-like infixl 6 _+_
-- negation-like infix 8 ¬_
-- and-like infixr 7 _∧_
-- or-like infixr 6 _∨_
-- post-fix inverse infix 8 _⁻¹
-- bind infixl 1 _>>=_
-- list concat-like infixr 5 _∷_
-- ternary reasoning infix 1 _⊢_≈_
-- composition infixr 9 _∘_
-- application infixr -1 _$_ _$!_
-- combinatorics infixl 6.5 _P_ _P′_ _C_ _C′_
-- pair infixr 4 _,_
-- Reasoning:
-- QED infix 3 _∎
-- stepping infixr 2 _≡⟨⟩_ step-≡ step-≡˘
-- begin infix 1 begin_
-- type formers:
-- product-like infixr 2 _×_ _-×-_ _-,-_
-- sum-like infixr 1 _⊎_
-- binary properties infix 4 _Absorbs_
|
