l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Assistant de preuve
58 Commits 1 Branch 0 Tags 973 KiB
OCaml 63.7%
TeX 31.7%
Roff 2.2%
Shell 2%
Makefile 0.4%
main
Go to file
augustin64 2be72fd16d Update README
2024-05-20 20:59:14 +02:00
RapportPresentation derniers changements du rapport et catch de Not_found 2024-05-20 16:32:42 +02:00
tests Remove tests 2024-05-20 20:56:26 +02:00
.gitignore Update .gitignore 2024-05-16 11:30:13 +02:00
affichage.ml on force l'annotation sur le OU 2024-05-17 08:10:26 +02:00
dune implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00
dune-project initial commit 2024-04-09 11:09:33 +02:00
hlam.ml Add comments for Undo, get_instr 2024-05-20 14:51:40 +02:00
lam.ml on force l'annotation sur le OU 2024-05-17 08:10:26 +02:00
lexer.mll implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00
main.ml Fix Undo try 2024-05-20 15:03:50 +02:00
Makefile ajout du système de preuve et implémentation des tactiques exact, intro, cut et apply 2024-04-25 10:11:08 +02:00
parser_entry.ml implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00
parser.mly implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00
proof.ml Fix Undo try 2024-05-20 15:03:50 +02:00
README.md Update README 2024-05-20 20:59:14 +02:00
tests.sh Add bad 8pus files 2024-05-20 10:57:55 +02:00
types.ml implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00
typing.ml derniers changements du rapport et catch de Not_found 2024-05-20 16:32:42 +02:00

README.md

Compilation et execution

pour (re)compiler, lancer

make

pour executer le programme, lancer

./pieuvre

pour lancer la batterie de tests:

./tests.sh