A prelude for Agda based on the Standard Library.
Added some comments.
Added _⊎-<-isStrictTotalOrder_ and _⊎-<-strictTotalOrder_.
Added a README for the AVL tree module.
Added case_of_ and some examples (empty was suggested by Ulf Norell).
Added from-yes and from-no. Removed fromYes and fromYes-map-commute.
Made difference lists/vectors and AVL trees universe polymorphic.
Added a search tree invariant to the implementation of AVL trees.
Added inspect on steroids. Deprecated the old inspect idiom.
GenerateEverything now uses UTF8 when reading/writing Agda files.
Added ≡⇒ and EquationalReasoning._≡⟨_⟩_.
Removed all occurrences of the --universe-polymorphism flag.
Added header lines containing "The Agda standard library".
Modified a comment.
Removed forced and non-strict.
Removed HeterogeneousEquality. Added PropositionalEquality.
Updated code to reflect changes to Agda.
Rolled back experiment.
Experiment: Represented kinds with equality in a different way.
© too generic 2010—2011
follow me on twitter