Recent searches
Search options
At the #agda headquaters:
"OK, guys, so our user pool consists only of folks who already know #haskell and #emacs Is there a way to narrow it down more?"
"I got it, what if we allow unicode, so they also have to also know #latex ?"
"Brilliant!"
(just kidding, agda is very cool (hope to learn it someday))
@abuseofnotation I REALLY want to learn it but Haskell is as advanced as I go at the moment.
@harryprayiv @abuseofnotation If you know Haskell, Agda is honestly not that bad. Yes, it’s more complicated, but much of the mindset is similar, as proofs are usually just ordinary recursive functions, using pattern matching to destruct the data structure.
for natural numbers, a recursive function corresponds exactly to classical induction proofs:
someProof : (n : Nat) -> SomeProperty n
someProof zero = baseCase
someProof (suc n) = inductionStep n (someProof n)
@LambdaDuck @harryprayiv Yeah, it's a pity that a language with such a simple core ended up so complex.