blob: b6850a85182966d8efeb2c570f1e3485c2e5d385 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Version 0.11
============
The library has been tested using Agda version 2.4.2.4.
Important changes since 0.10:
* `Relation.Binary.PropositionalEquality.TrustMe.erase` was added.
* Added `Data.Nat.Base.{_≤″_,_≥″_,_<″_,_>″_,erase}`,
`Data.Nat.Properties.{≤⇒≤″,≤″⇒≤}`, `Data.Fin.fromℕ≤″`, and
`Data.Fin.Properties.fromℕ≤≡fromℕ≤″`.
* The functions in `Data.Nat.DivMod` have been optimised.
* Turned on η-equality for `Record.Record`, removed
`Record.Signature′` and `Record.Record′`.
* Renamed `Data.AVL.agda._⊕_sub1` to `pred[_⊕_]`.
|
