GitHub - xplat/potpourri: things too small to be separate projects

xplat / potpourri Public

Notifications You must be signed in to change notification settings
Fork 0
Star 4

things too small to be separate projects

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 23 Commits
Fast		Fast
Primes		Primes
AltEquality.agda		AltEquality.agda
Altivec.agda		Altivec.agda
CantCountCantor.agda		CantCountCantor.agda
Denum.agda		Denum.agda
ELens.hs		ELens.hs
Golforth.hs		Golforth.hs
IxNat.agda		IxNat.agda
IxNatEx.agda		IxNatEx.agda
Lifts.hs		Lifts.hs
MLens.hs		MLens.hs
PatriciaTrie.agda		PatriciaTrie.agda
README		README
Trie.hs		Trie.hs
extract-urls.pl		extract-urls.pl
patmv.pl		patmv.pl

Repository files navigation

* AltEquality.agda - A sort of Church-encoded propositional equality.

* Altivec.agda - Vecs with eta.

* CantCountCantor.agda - 2^&#x2135;₀ ≠ &#x2135;₀.

* Denum.agda - Equality and ordering from an injection into the naturals.

* extract-urls.pl - extract urls from chat logs

* Golforth.hs - Point-free Haskell the Forth way.

* IxNat.agda - A small sample of what first-class ornaments would be like?

* IxNatEx.agda - IxNat.agda in action: naturals indexed by parity, Even and Odd.

* patmv.pl - Rename multiple files with regex replacements.

* PatriciaTrie.agda - Bitvector-indexed tries.

  A response to http://www.reddit.com/r/dependent_types/comments/qmlml/patricia_trie_challenge/ .

* Primes/ - Fast (relatively speaking) Sieve of Eratosthenes in Agda

  Currently unproven, but can compute primes at least as high as 2741 practically by normalization in Emacs.  The files FastNat.agda and Heap.agda seem especially likely to be reusable by other projects.

* Trie.hs - Is Haskell more readable than python?

  A response to some other reddit post comparing readability of Haskell and python in the case of tries.