Hacker GitHub

← All repos

agda/agda-stdlib

View on GitHub ↗ ★ 680 Agda

The Agda standard library

7 mentions on Hacker News by 5 people: 0 stories, 7 comments · first 2014-04-16 · latest 2020-08-18

Mentions per year 7 mentions · busiest year 2014 (2)
20082026
AllStoriesComments NewestTopOldest
  1. …usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre... Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blo…
    comment by gnulinux · 2020-08-18 · in APL386 Unicode – An APL Font
  2. …type, where `suc = just` and `zero = nothing`. You can see an example implementation of it in Agda: https://github.com/agda/agda-stdlib/blob/master/src/Codata/C... As to what is the practical implications of a Conat class? You can use it…
    comment by gnulinux · 2020-07-17 · in Forbidden Haskell Types
  3. …Agda plugin. In Agda using Unicode identifiers is widely accepted, even in the standard library: https://github.com/agda/agda-stdlib/blob/master/src/Relation...
    comment by danidiaz · 2019-06-08 · in Rust, Macros, λ-calculus/Church numerals, oh my
  4. …in a way that provides evidence that it halts. This can get very messy very quickly (e.g. see https://github.com/agda/agda-stdlib/blob/master/src/Relation... ). So the resulting program will be a massive pile of symbols, all carefully…
    comment by chriswarbo · 2018-07-05 · in Why I Don't Love Gödel, Escher, Bach
  5. …you are still interested. [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...
    comment by pka · 2016-09-22 · in Hacker-Proof Code Confirmed
  6. …but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation...
    comment by tel · 2014-07-02 · in Dependently Typed Programming
  7. …than Agda will be absolutely no harder. Go take a look at the Agda standard library to get a taste: https://github.com/agda/agda-stdlib Something like Relation.Binary.Core is a good place to start: https://github.com/agda/agda-stdlib/blob/m…
    comment by tel · 2014-04-16 · in Agda by Example: Sorting