Index of /~monin/Enseignement/Misc/MCAL/install_coq_perso

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory  -  
[TXT]README.html2024-03-31 17:06 2.2K 
[TXT]README.md2024-03-31 17:06 1.4K 
[DIR]Version_compilee_8.11/2024-03-31 17:06 -  
[DIR]Version_compilee_8.13/2024-03-31 17:06 -  
[DIR]Version_compilee_IM2AG_8.9/2024-03-31 17:06 -  
[DIR]Version_compilee_coq-8.15_OCaml-4.11.1/2024-03-31 17:06 -  
[DIR]Version_compilee_coq-8.15_OCaml-4.13.1/2024-03-31 17:06 -  
[TXT]untypedLC.v2024-03-31 17:06 43K 
[   ]untypedLC.v.gz2024-03-31 17:06 9.2K 

MCAL λ README install

Il faut avoir préalablement installé Coq en suivant par exemple les instructions données dans

http://www-verimag.imag.fr/~monin/Enseignement/LTPF/robuste/commun/installation/install.html

Ces instructions permettent en fait d’installer un environnement plus complet comprenant, en dehors de coq et de l’interface coqide (disponibles aussi sur les machine IM2AG), une autre interface pour emacs appelée proof-general ainsi que le langage OCaml.

Le présent répertoire contient un fichier coq à utiliser pour expérimenter du λ-calcul non typé en Coq. Attention, vous devez disposer d’une version de Coq suffisamment récente (8.9 ou suivantes). Ce n’est pas forcément le cas de la version de Coq fournie par les paquetages de Debian ou Ubuntu. Il faut au final obtenir un fichier untypedLC.vo (du coq préalablement compilé) dans le répertoire de travail.

Différents formats sont proposés :

Version html de cette page produite par :
pandoc -s --metadata pagetitle="MCAL λ README install" -o README.html README.md