On Fri, 28 Sep 2007, Jeff Polakow [EMAIL PROTECTED] wrote:
Agda is essentially an implementation of a type checker for
Martin-Lof type theory (i.e. dependent types).
It is designed to be used as a proof assistant.
Well, the language aims to become a practical programming language.
Ulf's
dons has been posting some links regarding agda on reddit. fairly
interesting, a quick glance and you think you are reading haskell
code.
does anyone have any insights on the major differences in these
languages?
___
Haskell-Cafe mailing list
On Friday 28 September 2007, brad clawsie wrote:
dons has been posting some links regarding agda on reddit. fairly
interesting, a quick glance and you think you are reading haskell
code.
does anyone have any insights on the major differences in these
languages?
I'm not too familiar with
Hello,
Agda is essentially an implementation of a type checker for Martin-Lof
type theory (i.e. dependent types).
It is designed to be used as a proof assistant. Roughly speaking
propositions are represented as types and a proof of a proposition is a
well-typed, total and terminating
