File tree 8 files changed +7
-19
lines changed
8 files changed +7
-19
lines changed Original file line number Diff line number Diff line change 1
1
Version 1.7.3
2
2
=============
3
3
4
- The library has been tested using Agda 2.6.4.
4
+ The library has been tested using Agda 2.6.3 & 2.6. 4.
5
5
6
6
* To avoid _ large indices_ that are by default no longer allowed in Agda 2.6.4,
7
7
universe levels have been increased in the following definitions:
Original file line number Diff line number Diff line change @@ -5,5 +5,5 @@ The library has been tested using Agda 2.6.3.
5
5
6
6
* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
7
7
the ` --without-K ` flag now use the ` --cubical-compatible ` flag instead.
8
-
8
+
9
9
* Updated the code using ` primFloatToWord64 ` - the library API has remained unchanged.
Original file line number Diff line number Diff line change 4
4
- name : " The Agda Community"
5
5
title : " Agda Standard Library"
6
6
version : 1.7.3
7
- date-released : 2023-10-15
7
+ date-released : 2023-10-13
8
8
url : " https://github.com/agda/agda-stdlib"
Original file line number Diff line number Diff line change 1
1
Installation instructions
2
2
=========================
3
3
4
- Use version v1.7.3 of the standard library with Agda 2.6.4.
4
+ Use version v1.7.3 of the standard library with Agda 2.6.3 or 2.6. 4.
5
5
6
6
1 . Navigate to a suitable directory ` $HERE ` (replace appropriately) where
7
7
you would like to install the library.
Load Diff This file was deleted.
Original file line number Diff line number Diff line change 5
5
-- for forward compatibility with v2.0.
6
6
------------------------------------------------------------------------
7
7
8
- {-# OPTIONS --cubical-compatible --safe #-}
8
+ {-# OPTIONS --cubical-compatible --safe --guardedness #-}
9
9
10
10
module Effect.Monad.Partiality where
11
11
Original file line number Diff line number Diff line change 5
5
-- for forward compatibility with v2.0.
6
6
------------------------------------------------------------------------
7
7
8
- {-# OPTIONS --cubical-compatible --safe #-}
8
+ {-# OPTIONS --cubical-compatible --safe --guardedness #-}
9
9
10
10
module Effect.Monad.Partiality.All where
11
11
Original file line number Diff line number Diff line change 5
5
-- for forward compatibility with v2.0.
6
6
------------------------------------------------------------------------
7
7
8
- {-# OPTIONS --cubical-compatible --safe #-}
8
+ {-# OPTIONS --cubical-compatible --safe --guardedness #-}
9
9
10
10
module Effect.Monad.Partiality.Instances where
11
11
You can’t perform that action at this time.
0 commit comments