Package: agda (2.6.2.2-1.1)

[ Source: agda  ]

linguagem de programação funcional com tipagem dependente

Agda é uma linguagem de programação funcional com tipagem dependente: ela possui famílias indutivas, que são similares a GADTs do Haskell, mas podem ser indexadas por valores e não somente por tipos. Ela também possui módulos parametrizáveis, operadores "mixfix", caracteres Unicode e uma interface Emacs interativa (o verificador de tipos pode ajudá-lo no desenvolvimento de seu código).

Agda também é um assistente de provas: ela é um sistema interativo para escrever e verificar provas. Agda é baseada na teoria de tipos intuicionística, um sistema fundacional para matemática construtiva desenvolvido pelo lógico sueco Per Martin-Löf. Ela possui muitas similaridades com outros assistentes de provas baseados em tipos dependentes tais como Coq, Epigram e NuPRL.

Este é um meta-pacote que fornece o modo de emacs Agda, o executável, a biblioteca padrão e sua documentação.

Tags: Role: Metapackage

Other Packages Related to agda

• dep: agda-bin

  commandline interface to Agda

• dep: agda-stdlib

  standard library for Agda

• dep: agda-stdlib-doc

  standard library for Agda — documentation

• dep: elpa-agda2-mode

  dependently typed functional programming language — emacs mode

• dep: libghc-agda-dev

  dependently typed functional programming language

Download agda

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	12.0 kB	20.0 kB	[list of files]