toutes les options
[  buster  ] [  bullseye  ] [  bookworm  ] [  trixie  ] [  sid  ]
[ Paquet source : agda  ]

Paquet : elpa-agda2-mode (2.6.3-1)

Liens pour elpa-agda2-mode

Screenshot

Ressources Debian :

Télécharger le paquet source agda :

Responsable :

Ressources externes :

Paquets similaires :

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

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 mode de développement interactif pour emacs. Ce mode est la méthode recommandée pour écrire du code Agda ; il possède des fonctionnalités comme le développement itératif, le raffinement, l'analyse de cas et bien d'autres encore.

Autres paquets associés à elpa-agda2-mode

  • dépendances
  • recommandations
  • suggestions
  • enhances

Télécharger elpa-agda2-mode

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
all 57,9 ko221,0 ko [liste des fichiers]