Paquet : agda-stdlib (2.1-3)

[ Paquet source : agda-stdlib  ]

bibliothèque standard pour Agda

Agda est un langage de programmation fonctionnel typé de façon dépendante. Il possède des familles inductives, qui ressemblent aux GADT de Haskell, mais qui peuvent être indexées par des valeurs et pas seulement des types. Il possède également des modules de paramétrisations, des opérateurs mixfix, les caractères Unicode et une interface Emacs interactive (le vérificateur de type peut aider au développement du code).

Agda est également un assistant de preuve : c'est un système interactif pour écrire et vérifier des preuves. Agda est basé sur la théorie des types intuitifs, un système fondamental pour les mathématiques constructives développé par le logicien suédois Per Martin-Löf. Il possède de nombreux points communs avec d'autres assistants de preuves basés sur des types dépendants comme Coq, Epigram et NuPRL.

La bibliothèque standard d'Agda contient des modules pour beaucoup de structures de données communes et de motifs de preuve. Les modules fournis contiennent :

 - Algebra : spécifie et raisonne sur des structures algébriques
    abstraites ;
 - Category : utilise des idiomes de la théorie des catégories pour
    structurer des programmes fonctionnels ;
 - Coinduction : gestion de la programmation coinductive ;
 - Data : types de données et propriétés des types de données ;
 - Foreign : relatif à l'interface de fonctions étrangères ;
 - Induction : cadre applicatif général pour l'induction ;
 - IO : fonctions relatives aux entrées/sorties ;
 - Level : niveaux universels ;
 - Relations : preuves et propriétés sur des relations ;
 - Size : tailles utilisées par le mécanisme de types avec tailles.

Ce paquet fournit la bibliothèque complète.

Étiquettes: Rôle: Bibliothèque partagée

Autres paquets associés à agda-stdlib

• dep: libghc-agda-dev (<< 2.6.4.4~)

  langage de programmation fonctionnel typé de façon dépendante

  dep: libghc-agda-dev (>= 2.6.4.3)

• enh: elpa-agda2-mode

  langage de programmation fonctionnel typé de façon dépendante - mode emacs

Télécharger agda-stdlib

Télécharger pour toutes les architectures proposées

Architecture	Taille du paquet	Espace occupé une fois installé	Fichiers
all	136 445,4 ko	179 538,0 ko	[liste des fichiers]