Skip to content

Commit 4636ee6

Browse files
HeinrichApfelmusHeinrichApfelmus
committed
Apply review suggestions
Co-authored by: Orestis Melkonian <melkon.or@gmail.com>
1 parent 7122057 commit 4636ee6

File tree

7 files changed

+103
-99
lines changed

7 files changed

+103
-99
lines changed

‎lib/containers/agda/Data/Map/Prop.agda

+11-10
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,14 @@ open import Haskell.Data.Maybe using
1414

1515
import Data.Map.Maybe as Maybe
1616
import Haskell.Prelude as List using (map)
17+
open import Data.Set using (Set)
1718
import Data.Set as Set
1819

1920
{-----------------------------------------------------------------------------
2021
Proofs
2122
involving 1 value type
2223
------------------------------------------------------------------------------}
23-
module _ {k a : Set} {{_ : Ord k}} where
24+
module _ {k a : Type} {{_ : Ord k}} where
2425

2526
--
2627
prop-member-null
@@ -210,7 +211,7 @@ module _ {k a : Set} {{_ : Ord k}} where
210211
Proofs
211212
involving keysSet
212213
------------------------------------------------------------------------------}
213-
module _ {k a : Set} {{_ : Ord k}} where
214+
module _ {k a : Type} {{_ : Ord k}} where
214215

215216
--
216217
prop-member-keysSet
@@ -355,11 +356,11 @@ module _ {k a : Set} {{_ : Ord k}} where
355356
Proofs
356357
involving withoutKeys and restrictKeys
357358
------------------------------------------------------------------------------}
358-
module _ {k a : Set} {{_ : Ord k}} where
359+
module _ {k a : Type} {{_ : Ord k}} where
359360

360361
--
361362
prop-lookup-withoutKeys
362-
: ∀ (key : k) (m : Map k a) (ks : Set.ℙ k)
363+
: ∀ (key : k) (m : Map k a) (ks : Set k)
363364
→ lookup key (withoutKeys m ks)
364365
≡ Maybe.filt (not (Set.member key ks)) (lookup key m)
365366
--
@@ -377,7 +378,7 @@ module _ {k a : Set} {{_ : Ord k}} where
377378

378379
--
379380
prop-lookup-restrictKeys
380-
: ∀ (key : k) (m : Map k a) (ks : Set.ℙ k)
381+
: ∀ (key : k) (m : Map k a) (ks : Set k)
381382
→ lookup key (restrictKeys m ks)
382383
≡ Maybe.filt (Set.member key ks) (lookup key m)
383384
--
@@ -441,7 +442,7 @@ module _ {k a : Set} {{_ : Ord k}} where
441442

442443
--
443444
prop-restrictKeys-union
444-
: ∀ (ma mb : Map k a) (ks : Set.ℙ k)
445+
: ∀ (ma mb : Map k a) (ks : Set k)
445446
→ restrictKeys (union ma mb) ks
446447
≡ union (restrictKeys ma ks) (restrictKeys mb ks)
447448
--
@@ -499,7 +500,7 @@ module _ {k a : Set} {{_ : Ord k}} where
499500

500501
--
501502
prop-withoutKeys-union
502-
: ∀ (ma mb : Map k a) (ks : Set.ℙ k)
503+
: ∀ (ma mb : Map k a) (ks : Set k)
503504
→ withoutKeys (union ma mb) ks
504505
≡ union (withoutKeys ma ks) (withoutKeys mb ks)
505506
--
@@ -531,7 +532,7 @@ module _ {k a : Set} {{_ : Ord k}} where
531532

532533
--
533534
prop-withoutKeys-difference
534-
: ∀ (m : Map k a) (ka kb : Set.ℙ k)
535+
: ∀ (m : Map k a) (ka kb : Set k)
535536
→ withoutKeys m (Set.difference ka kb)
536537
≡ union (withoutKeys m ka) (restrictKeys m kb)
537538
--
@@ -582,7 +583,7 @@ module _ {k a : Set} {{_ : Ord k}} where
582583

583584
--
584585
prop-withoutKeys-withoutKeys
585-
: ∀ (m : Map k a) (ka kb : Set.ℙ k)
586+
: ∀ (m : Map k a) (ka kb : Set k)
586587
→ withoutKeys (withoutKeys m ka) kb
587588
≡ withoutKeys m (Set.union ka kb)
588589
--
@@ -625,7 +626,7 @@ module _ {k a : Set} {{_ : Ord k}} where
625626

626627
--
627628
@0 prop-withoutKeys-intersection
628-
: ∀ (m : Map k a) (ka kb : Set.ℙ k)
629+
: ∀ (m : Map k a) (ka kb : Set k)
629630
→ withoutKeys m (Set.intersection ka kb)
630631
≡ union (withoutKeys m ka) (withoutKeys m kb)
631632
--

‎lib/containers/agda/Data/Set/Prop.agda

+30-30
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# OPTIONS --erasure #-}
1+
{-# OPTIONS --erasure --no-import-sorts #-}
22

33
-- | Proofs on 'Set'.
44
module Data.Set.Prop where
@@ -13,7 +13,7 @@ open import Haskell.Data.Set
1313
Properties
1414
Basic
1515
------------------------------------------------------------------------------}
16-
module _ {a : Set} {{_ : Ord a}} where
16+
module _ {a : Type} {{_ : Ord a}} where
1717

1818
--
1919
prop-null-empty
@@ -26,11 +26,11 @@ module _ {a : Set} {{_ : Ord a}} where
2626
Properties
2727
https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
2828
------------------------------------------------------------------------------}
29-
module _ {a : Set} {{_ : Ord a}} where
29+
module _ {a : Type} {{_ : Ord a}} where
3030

3131
--
3232
prop-union-idem
33-
: ∀ {sa : ℙ a}
33+
: ∀ {sa : Set a}
3434
→ union sa sa
3535
≡ sa
3636
--
@@ -46,7 +46,7 @@ module _ {a : Set} {{_ : Ord a}} where
4646

4747
--
4848
prop-union-assoc
49-
: ∀ {sa sb sc : ℙ a}
49+
: ∀ {sa sb sc : Set a}
5050
→ union (union sa sb) sc
5151
≡ union sa (union sb sc)
5252
--
@@ -66,7 +66,7 @@ module _ {a : Set} {{_ : Ord a}} where
6666

6767
--
6868
prop-union-sym
69-
: ∀ {sa sb : ℙ a}
69+
: ∀ {sa sb : Set a}
7070
→ union sa sb
7171
≡ union sb sa
7272
--
@@ -83,7 +83,7 @@ module _ {a : Set} {{_ : Ord a}} where
8383

8484
--
8585
prop-union-absorb
86-
: ∀ {sa sb : ℙ a}
86+
: ∀ {sa sb : Set a}
8787
→ union sa (intersection sa sb)
8888
≡ sa
8989
--
@@ -100,7 +100,7 @@ module _ {a : Set} {{_ : Ord a}} where
100100

101101
--
102102
prop-union-identity
103-
: ∀ {sa : ℙ a}
103+
: ∀ {sa : Set a}
104104
→ union sa empty
105105
≡ sa
106106
--
@@ -117,7 +117,7 @@ module _ {a : Set} {{_ : Ord a}} where
117117

118118
--
119119
prop-union-intersection-distribute
120-
: ∀ {sa sb sc : ℙ a}
120+
: ∀ {sa sb sc : Set a}
121121
→ union sa (intersection sb sc)
122122
≡ intersection (union sa sb) (union sa sc)
123123
--
@@ -139,7 +139,7 @@ module _ {a : Set} {{_ : Ord a}} where
139139

140140
--
141141
prop-intersection-idem
142-
: ∀ {sa : ℙ a}
142+
: ∀ {sa : Set a}
143143
→ intersection sa sa
144144
≡ sa
145145
--
@@ -155,7 +155,7 @@ module _ {a : Set} {{_ : Ord a}} where
155155

156156
--
157157
prop-intersection-assoc
158-
: ∀ {sa sb sc : ℙ a}
158+
: ∀ {sa sb sc : Set a}
159159
→ intersection (intersection sa sb) sc
160160
≡ intersection sa (intersection sb sc)
161161
--
@@ -175,7 +175,7 @@ module _ {a : Set} {{_ : Ord a}} where
175175

176176
--
177177
prop-intersection-sym
178-
: ∀ {sa sb : ℙ a}
178+
: ∀ {sa sb : Set a}
179179
→ intersection sa sb
180180
≡ intersection sb sa
181181
--
@@ -192,7 +192,7 @@ module _ {a : Set} {{_ : Ord a}} where
192192

193193
--
194194
prop-intersection-absorb
195-
: ∀ {sa sb : ℙ a}
195+
: ∀ {sa sb : Set a}
196196
→ intersection sa (union sa sb)
197197
≡ sa
198198
--
@@ -209,7 +209,7 @@ module _ {a : Set} {{_ : Ord a}} where
209209

210210
--
211211
prop-intersection-union-distribute
212-
: ∀ {sa sb sc : ℙ a}
212+
: ∀ {sa sb sc : Set a}
213213
→ intersection sa (union sb sc)
214214
≡ union (intersection sa sb) (intersection sa sc)
215215
--
@@ -230,7 +230,7 @@ module _ {a : Set} {{_ : Ord a}} where
230230

231231
--
232232
prop-intersection-empty-right
233-
: ∀ {sa : ℙ a}
233+
: ∀ {sa : Set a}
234234
→ intersection sa empty
235235
≡ empty
236236
--
@@ -247,7 +247,7 @@ module _ {a : Set} {{_ : Ord a}} where
247247

248248
--
249249
prop-intersection-empty-left
250-
: ∀ {sa : ℙ a}
250+
: ∀ {sa : Set a}
251251
→ intersection empty sa
252252
≡ empty
253253
--
@@ -265,11 +265,11 @@ module _ {a : Set} {{_ : Ord a}} where
265265
Properties
266266
involving difference
267267
------------------------------------------------------------------------------}
268-
module _ {a : Set} {{_ : Ord a}} where
268+
module _ {a : Type} {{_ : Ord a}} where
269269

270270
--
271271
prop-intersection-difference
272-
: ∀ {sa sb : ℙ a}
272+
: ∀ {sa sb : Set a}
273273
→ intersection sb (difference sa sb)
274274
≡ empty
275275
--
@@ -291,7 +291,7 @@ module _ {a : Set} {{_ : Ord a}} where
291291

292292
--
293293
prop-disjoint-difference
294-
: ∀ {sa sb : ℙ a}
294+
: ∀ {sa sb : Set a}
295295
→ disjoint sb (difference sa sb)
296296
≡ True
297297
--
@@ -300,7 +300,7 @@ module _ {a : Set} {{_ : Ord a}} where
300300

301301
--
302302
prop-union-difference
303-
: ∀ {sa sb : ℙ a}
303+
: ∀ {sa sb : Set a}
304304
→ union (difference sa sb) sb
305305
≡ union sa sb
306306
--
@@ -323,7 +323,7 @@ module _ {a : Set} {{_ : Ord a}} where
323323

324324
--
325325
prop-difference-union-x
326-
: ∀ {sa sb sc : ℙ a}
326+
: ∀ {sa sb sc : Set a}
327327
→ difference (union sa sb) sc
328328
≡ union (difference sa sc) (difference sb sc)
329329
--
@@ -347,7 +347,7 @@ module _ {a : Set} {{_ : Ord a}} where
347347

348348
--
349349
prop-deMorgan-difference-intersection
350-
: ∀ {sa sb sc : ℙ a}
350+
: ∀ {sa sb sc : Set a}
351351
→ difference sa (intersection sb sc)
352352
≡ union (difference sa sb) (difference sa sc)
353353
--
@@ -369,7 +369,7 @@ module _ {a : Set} {{_ : Ord a}} where
369369

370370
--
371371
prop-deMorgan-difference-union
372-
: ∀ {sa sb sc : ℙ a}
372+
: ∀ {sa sb sc : Set a}
373373
→ difference sa (union sb sc)
374374
≡ intersection (difference sa sb) (difference sa sc)
375375
--
@@ -393,27 +393,27 @@ module _ {a : Set} {{_ : Ord a}} where
393393
Properties
394394
involving isSubsetOf
395395
------------------------------------------------------------------------------}
396-
module _ {a : Set} {{_ : Ord a}} where
396+
module _ {a : Type} {{_ : Ord a}} where
397397

398398
-- | The 'empty' set is a subset of every set.
399399
prop-isSubsetOf-empty
400-
: ∀ {sa : ℙ a}
400+
: ∀ {sa : Set a}
401401
→ isSubsetOf empty sa ≡ True
402402
--
403403
prop-isSubsetOf-empty {sa} =
404404
prop-intersection→isSubsetOf empty sa prop-intersection-empty-left
405405

406406
-- | 'isSubsetOf' is reflexive
407407
prop-isSubsetOf-refl
408-
: ∀ {sa : ℙ a}
408+
: ∀ {sa : Set a}
409409
→ isSubsetOf sa sa ≡ True
410410
--
411411
prop-isSubsetOf-refl {sa} =
412412
prop-intersection→isSubsetOf sa sa prop-intersection-idem
413413

414414
-- | 'isSubsetOf' is antisymmetric
415415
prop-isSubsetOf-antisym
416-
: ∀ {sa sb : ℙ a}
416+
: ∀ {sa sb : Set a}
417417
→ isSubsetOf sa sb ≡ True
418418
→ isSubsetOf sb sa ≡ True
419419
→ sa ≡ sb
@@ -440,7 +440,7 @@ module _ {a : Set} {{_ : Ord a}} where
440440

441441
-- | 'isSubsetOf' is transitive
442442
prop-isSubsetOf-trans
443-
: ∀ {sa sb sc : ℙ a}
443+
: ∀ {sa sb sc : Set a}
444444
→ isSubsetOf sa sb ≡ True
445445
→ isSubsetOf sb sc ≡ True
446446
→ isSubsetOf sa sc ≡ True
@@ -471,7 +471,7 @@ module _ {a : Set} {{_ : Ord a}} where
471471

472472
--
473473
prop-isSubsetOf-intersection
474-
: ∀ {sa sb : ℙ a}
474+
: ∀ {sa sb : Set a}
475475
→ isSubsetOf (intersection sa sb) sb ≡ True
476476
--
477477
prop-isSubsetOf-intersection {sa} {sb} =
@@ -487,7 +487,7 @@ module _ {a : Set} {{_ : Ord a}} where
487487

488488
--
489489
prop-isSubsetOf-difference
490-
: ∀ {sa sb : ℙ a}
490+
: ∀ {sa sb : Set a}
491491
→ isSubsetOf (difference sa sb) sa ≡ True
492492
--
493493
prop-isSubsetOf-difference {sa} {sb} =

‎lib/containers/agda/EverythingContainers.agda

-4
This file was deleted.

0 commit comments

Comments
 (0)