Skip to content

Commit 3768134

Browse files
Saransh-cppSofia-Insa
Saransh-cpp
and
Sofia-Insa
authored
Add new fixities (#2116)
Co-authored-by: Sofia El Boufi--Crouzet <[email protected]>
1 parent d937ace commit 3768134

File tree

28 files changed

+94
-13
lines changed

28 files changed

+94
-13
lines changed

‎CHANGELOG.md

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,34 @@ Bug-fixes
120120
infixl 6 _+ℤ_ (Relation.Binary.HeterogeneousEquality.Quotients.Examples)
121121
infix 4 _≉_ _≈ᵢ_ _≤ᵢ_ (Relation.Binary.Indexed.Homogeneous.Bundles)
122122
infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_ (Text.Regex.Search)
123+
infixr 4 _,_ (Data.Refinement)
124+
infixr 4 _,_ (Data.Container.Relation.Binary.Pointwise)
125+
infixr 4 _,_ (Data.Tree.AVL.Value)
126+
infixr 4 _,_ (Foreign.Haskell.Pair)
127+
infixr 4 _,_ (Reflection.AnnotatedAST)
128+
infixr 4 _,_ (Reflection.AST.Traversal)
129+
infixl 6.5 _P′_ _P_ _C′_ _C_ (Data.Nat.Combinatorics.Base)
130+
infixl 1 _>>=-cong_ _≡->>=-cong_ (Effect.Monad.Partiality)
131+
infixl 1 _?>=′_ (Effect.Monad.Predicate)
132+
infixl 1 _>>=-cong_ _>>=-congP_ (Effect.Monad.Partiality.All)
133+
infix 4 _∈FV_ (Reflection.AST.DeBruijn)
134+
infixr 9 _;_ (Relation.Binary.Construct.Composition)
135+
infixl 6 _+²_ (Relation.Binary.HeterogeneousEquality.Quotients.Examples)
136+
infixr -1 _atₛ_ (Relation.Binary.Indexed.Heterogeneous.Construct.At)
137+
infixr -1 _atₛ_ (Relation.Binary.Indexed.Homogeneous.Construct.At)
138+
infix 4 _∈_ _∉_ (Relation.Unary.Indexed)
139+
infixr 9 _⍮_ (Relation.Unary.PredicateTransformer)
140+
infix 8 ∼_ (Relation.Unary.PredicateTransformer)
141+
infix 2 _×?_ _⊙?_ (Relation.Unary.Properties)
142+
infix 10 _~? (Relation.Unary.Properties)
143+
infixr 1 _⊎?_ (Relation.Unary.Properties)
144+
infixr 7 _∩?_ (Relation.Unary.Properties)
145+
infixr 6 _∪?_ (Relation.Unary.Properties)
146+
infixl 6 _`⊜_ (Tactic.RingSolver)
147+
infix 8 ⊝_ (Tactic.RingSolver.Core.Expression)
148+
infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_] (Text.Regex.Properties)
149+
infix 4 _∈?_ _∉?_ (Text.Regex.Derivative.Brzozowski)
150+
infix 4 _∈_ _∉_ _∈?_ _∉?_ (Text.Regex.String.Unsafe)
123151
```
124152

125153
* In `System.Exit`, the `ExitFailure` constructor is now carrying an integer

‎README/Design/Fixity.agda

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ module README.Design.Fixity where
2323
-- ternary reasoning infix 1 _⊢_≈_
2424
-- composition infixr 9 _∘_
2525
-- application infixr -1 _$_ _$!_
26+
-- combinatorics infixl 6.5 _P_ _P′_ _C_ _C′_
27+
-- pair infixr 4 _,_
2628

2729
-- Reasoning:
2830
-- QED infix 3 _∎

‎src/Data/Container/Relation/Binary/Pointwise.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ module _ {s p} (C : Container s p) where
2626
constructor _,_
2727
field shape : proj₁ cx ≡ proj₁ cy
2828
position : ∀ p → R (proj₂ cx p) (proj₂ cy (subst _ shape p))
29+
infixr 4 _,_
2930

3031
module _ {s p} {C : Container s p} {x y} {X : Set x} {Y : Set y}
3132
{ℓ ℓ′} {R : REL X Y ℓ} {R′ : REL X Y ℓ′}

‎src/Data/Nat/Combinatorics.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ nCk≡nC[n∸k] {k} {n} k≤n = begin-equality
7575
_ = k !* (n ∸ k) !≢0
7676
_ = (n ∸ k) !* (n ∸ (n ∸ k)) !≢0
7777

78-
nCk≡nPk/k! : k ≤ n → n C k ≡ (n P k / k !) {{k !≢0}}
78+
nCk≡nPk/k! : k ≤ n → n C k ≡ ((n P k) / k !) {{k !≢0}}
7979
nCk≡nPk/k! {k} {n} k≤n = begin-equality
8080
n C k ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩
8181
n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟩

‎src/Data/Nat/Combinatorics/Base.agda

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ open import Data.Nat.Properties using (_!≢0)
2525

2626
-- n P k = n ! / (n ∸ k) !
2727

28+
infixl 6.5 _P′_ _P_
29+
2830
-- Base definition. Only valid for k ≤ n.
2931

3032
_P′_ : ℕ → ℕ → ℕ
@@ -44,6 +46,8 @@ n P k = if k ≤ᵇ n then n P′ k else 0
4446

4547
-- n C k = n ! / (k ! * (n ∸ k) !)
4648

49+
infixl 6.5 _C′_ _C_
50+
4751
-- Base definition. Only valid for k ≤ n.
4852

4953
_C′_ : ℕ → ℕ → ℕ

‎src/Data/Nat/Combinatorics/Specification.agda

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -57,20 +57,20 @@ nP′k≡n[n∸1P′k∸1] : ∀ n k → .{{NonZero n}} → .{{NonZero k}} →
5757
nP′k≡n[n∸1P′k∸1] n (suc zero) = refl
5858
nP′k≡n[n∸1P′k∸1] n@(suc n-1) k@(suc k-1@(suc k-2)) = begin-equality
5959
n P′ k ≡⟨⟩
60-
(n ∸ k-1) * n P′ k-1 ≡⟨ cong ((n ∸ k-1) *_) (nP′k≡n[n∸1P′k∸1] n k-1) ⟩
61-
(n ∸ k-1) * (n * n-1 P′ k-2) ≡⟨ x∙yz≈y∙xz (n ∸ k-1) n (n-1 P′ k-2) ⟩
62-
n * ((n ∸ k-1) * n-1 P′ k-2) ≡⟨⟩
63-
n * n-1 P′ k-1 ∎
60+
(n ∸ k-1) * (n P′ k-1) ≡⟨ cong ((n ∸ k-1) *_) (nP′k≡n[n∸1P′k∸1] n k-1) ⟩
61+
(n ∸ k-1) * (n * (n-1 P′ k-2)) ≡⟨ x∙yz≈y∙xz (n ∸ k-1) n (n-1 P′ k-2) ⟩
62+
n * ((n ∸ k-1) * (n-1 P′ k-2)) ≡⟨⟩
63+
n * (n-1 P′ k-1) ∎
6464
where open ≤-Reasoning; open *-CS
6565

6666
P′-rec : ∀ {n k} → k ≤ n → .{{NonZero k}} →
6767
n P′ k ≡ k * (pred n P′ pred k) + pred n P′ k
6868
P′-rec n@{suc n-1} k@{suc k-1} k≤n = begin-equality
69-
n P′ k ≡⟨ nP′k≡n[n∸1P′k∸1] n k ⟩
70-
n * n-1 P′ k-1 ≡˘⟨ cong (_* n-1 P′ k-1) (m+[n∸m]≡n {k} {n} k≤n) ⟩
71-
(k + (n ∸ k)) * n-1 P′ k-1 ≡⟨ *-distribʳ-+ (n-1 P′ k-1) k (n ∸ k) ⟩
72-
k * (n-1 P′ k-1) + (n-1 ∸ k-1) * n-1 P′ k-1 ≡⟨⟩
73-
k * (n-1 P′ k-1) + n-1 P′ k ∎
69+
n P′ k ≡⟨ nP′k≡n[n∸1P′k∸1] n k ⟩
70+
n * (n-1 P′ k-1) ≡˘⟨ cong (_* (n-1 P′ k-1)) (m+[n∸m]≡n {k} {n} k≤n) ⟩
71+
(k + (n ∸ k)) * (n-1 P′ k-1) ≡⟨ *-distribʳ-+ (n-1 P′ k-1) k (n ∸ k) ⟩
72+
k * (n-1 P′ k-1) + (n-1 ∸ k-1) * (n-1 P′ k-1) ≡⟨⟩
73+
k * (n-1 P′ k-1) + (n-1 P′ k) ∎
7474
where open ≤-Reasoning
7575

7676
nP′n≡n! : ∀ n → n P′ n ≡ n !

‎src/Data/Refinement.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
2323
constructor _,_
2424
field value : A
2525
proof : Irrelevant (P value)
26+
infixr 4 _,_
2627
open Refinement public
2728

2829
-- The syntax declaration below is meant to mimick set comprehension.

‎src/Data/Tree/AVL/Value.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ record K&_ {v} (V : Value v) : Set (a ⊔ v) where
3434
field
3535
key : Key
3636
value : Value.family V key
37+
infixr 4 _,_
3738
open K&_ public
3839

3940
module _ {v} {V : Value v} where

‎src/Effect/Monad/Partiality.agda

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -517,6 +517,8 @@ module _ {A B : Set s}
517517

518518
-- Bind preserves all the relations.
519519

520+
infixl 1 _>>=-cong_
521+
520522
_>>=-cong_ :
521523
∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
522524
Rel _∼A_ k x₁ x₂ →
@@ -578,6 +580,8 @@ module _ {A B : Set ℓ} {_∼_ : B → B → Set ℓ} where
578580

579581
-- A variant of _>>=-cong_.
580582

583+
infixl 1 _≡->>=-cong_
584+
581585
_≡->>=-cong_ :
582586
∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
583587
Rel _≡_ k x₁ x₂ →

‎src/Effect/Monad/Partiality/All.agda

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ data All {A : Set a} (P : A → Set p) : A ⊥ → Set (a ⊔ p) where
4444

4545
-- Bind preserves All in the following way:
4646

47+
infixl 1 _>>=-cong_
48+
4749
_>>=-cong_ : ∀ {p q} {P : A → Set p} {Q : B → Set q}
4850
{x : A ⊥} {f : A → B ⊥} →
4951
All P x → (∀ {x} → P x → All Q (f x)) →
@@ -118,6 +120,8 @@ module Alternative {a p : Level} where
118120
_≳⟨_⟩P_ : ∀ x {y} (x≳y : x ≳ y) (p : AllP P y) → AllP P x
119121
_⟨_⟩P : ∀ x (p : AllP P x) → AllP P x
120122

123+
infixl 1 _>>=-congP_
124+
121125
private
122126

123127
-- WHNFs.

0 commit comments

Comments
 (0)