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[_⊕_]`.