changes

• Nils Anders Danielsson :: Sat Nov 19 15:30:54 UTC 2011

  Added some comments.

• Nils Anders Danielsson :: Sat Nov 19 15:30:35 UTC 2011

  Minor simplification.

• Nils Anders Danielsson :: Tue Nov 15 15:48:12 UTC 2011

  Added _⊎-<-isStrictTotalOrder_ and _⊎-<-strictTotalOrder_.

• Nils Anders Danielsson :: Fri Nov 11 19:05:33 UTC 2011

  More examples.

• Nils Anders Danielsson :: Fri Nov 11 18:45:50 UTC 2011

  Added a README for the AVL tree module.

• Nils Anders Danielsson :: Fri Nov 11 15:20:31 UTC 2011

  Added case_of_ and some examples (empty was suggested by Ulf Norell).

• Nils Anders Danielsson :: Fri Nov 4 15:35:18 UTC 2011

  Added Data.Nat.Primality.

• Nils Anders Danielsson :: Fri Nov 4 15:35:05 UTC 2011

  Added ¬?.

• Nils Anders Danielsson :: Fri Nov 4 15:30:50 UTC 2011

  Added from-yes and from-no. Removed fromYes and fromYes-map-commute.

• Nils Anders Danielsson :: Tue Oct 18 10:12:20 UTC 2011

  Made difference lists/vectors and AVL trees universe polymorphic.

• Nils Anders Danielsson :: Tue Oct 18 10:11:24 UTC 2011

  Added a search tree invariant to the implementation of AVL trees.

  • I also made the module telescope slightly more restrictive: the ordering relation's underlying equality now has to be propositional equality.

• Nils Anders Danielsson :: Thu Oct 6 13:49:29 UTC 2011

  Added inspect on steroids. Deprecated the old inspect idiom.

  • Inspect on steroids was invented by Ulf Norell.

• Nils Anders Danielsson :: Tue Oct 4 17:04:52 UTC 2011

  Removed Relation.Binary.HeterogeneousEquality.Inspect.

• Nils Anders Danielsson :: Sun Oct 2 17:18:59 UTC 2011

  GenerateEverything now uses UTF8 when reading/writing Agda files.

• Nils Anders Danielsson :: Fri Sep 30 07:58:18 UTC 2011

  Added Σ-assoc.

• Nils Anders Danielsson :: Thu Sep 29 08:32:02 UTC 2011

  Added ≡⇒ and EquationalReasoning._≡⟨_⟩_.

• Andrés Sicard-Ramírez :: Tue Sep 27 13:44:39 UTC 2011

  Cosmetic changes.

• Nils Anders Danielsson :: Sat Sep 24 17:11:17 UTC 2011

  Removed all occurrences of the --universe-polymorphism flag.

• Nils Anders Danielsson :: Mon Sep 19 16:04:32 UTC 2011

  Added header lines containing "The Agda standard library".

• Nils Anders Danielsson :: Mon Sep 19 15:26:11 UTC 2011

  Modified a comment.

• Nils Anders Danielsson :: Sun Sep 11 13:09:48 UTC 2011

  Removed forced and non-strict.

• Nils Anders Danielsson :: Fri Sep 9 07:51:33 UTC 2011

  Minor simplifications.

• Nils Anders Danielsson :: Thu Sep 8 14:31:46 UTC 2011

  Removed HeterogeneousEquality. Added PropositionalEquality.

• Nils Anders Danielsson :: Thu Sep 8 08:08:52 UTC 2011

  Updated code to reflect changes to Agda.

• Nils Anders Danielsson :: Thu Sep 8 06:40:35 UTC 2011

  Added case_return_of_.

  • Based on an idea from Ulf Norell.

• Nils Anders Danielsson :: Mon Sep 5 08:35:45 UTC 2011

  Removed Data.Context.

• Nils Anders Danielsson :: Tue Aug 30 12:06:08 UTC 2011

  Updated code to reflect changes to Agda.

• Nils Anders Danielsson :: Tue Aug 30 11:35:30 UTC 2011

  Added from-just.

• Nils Anders Danielsson :: Tue Aug 30 09:57:39 UTC 2011

  Rolled back experiment.

• Nils Anders Danielsson :: Tue Aug 30 09:57:20 UTC 2011

  Experiment: Represented kinds with equality in a different way.

• next ->
• page 1 of 38