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.
U
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 func
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 wit
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
Haskell-Ca
