Pacote: agda (2.6.4.3-1)

[ Fonte: 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.

Etiquetas: Função: Metapacotes

Outros pacotes relacionados a 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 de agda

Baixe para todas as arquiteturas disponíveis

Arquitetura	Tamanho do pacote	Tamanho instalado	Arquivos
all	11.9 kB	20.0 kB	[lista de arquivos]