Paquet : agda-bin (2.6.4.3-1)
Liens pour agda-bin
Ressources Debian :
- Rapports de bogues
- Developer Information
- Journal des modifications Debian
- Fichier de licence
- Suivis des correctifs pour Debian
Télécharger le paquet source agda :
Responsable :
Ressources externes :
- Page d'accueil [wiki.portal.chalmers.se]
Paquets similaires :
interface en ligne de commande 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.
Ce paquet fournit un programme en ligne de commande pour vérifier les types et compiler des programmes Agda. Ce programme peut également créer des fichiers HTML, avec la coloration syntaxique, depuis des sources Agda.
Autres paquets associés à agda-bin
|
|
|
|
-
- dep: libc6 (>= 2.38)
- bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6-udeb
-
- dep: libffi8 (>= 3.4)
- Bibliothèque d'exécution de l'interface de fonction étrangère (FFI)
-
- dep: libghc-agda-dev (<< 2.6.4.3+~)
- langage de programmation fonctionnel typé de façon dépendante
- dep: libghc-agda-dev (>= 2.6.4.3)
-
- dep: libgmp10 (>= 2:6.3.0+dfsg)
- Bibliothèque arithmétique à multi-précision
-
- dep: libnuma1 (>= 2.0.11)
- bibliothèques pour contrôler les politiques NUMA
-
- dep: libtinfo6 (>= 6)
- bibliothèque partagée terminfo de bas niveau pour manipuler le terminal
-
- dep: zlib1g (>= 1:1.1.4)
- Bibliothèque de compression - binaires
-
- sug: elpa-agda2-mode
- langage de programmation fonctionnel typé de façon dépendante - mode emacs
Télécharger agda-bin
Architecture | Taille du paquet | Espace occupé une fois installé | Fichiers |
---|---|---|---|
s390x | 19 309,6 ko | 143 968,0 ko | [liste des fichiers] |