Commit Graph

20 Commits

Author SHA1 Message Date
fc846d2233 Add tactic intros 2024-05-01 10:44:36 +02:00
7c4def6e1e gracefully ignore invalid input 2024-05-01 10:35:12 +02:00
486a788757 Parse exact term / proof 2024-04-30 11:58:29 +02:00
Marwan
20d4ee5531 on différencie exact pour les preuves et pour les termes 2024-04-30 11:56:41 +02:00
Marwan
ced6846dbc tactique try et intro 2024-04-30 11:48:26 +02:00
6063d33377 Add interactive proofs 2024-04-30 11:44:28 +02:00
Marwan
7195fc244f ajout du système de preuve et implémentation des tactiques exact, intro, cut et apply 2024-04-25 10:11:08 +02:00
Marwan
544a8bf093 on rend l'alpha conversion lisible en gardant les noms de variables 2024-04-25 04:33:42 +02:00
Marwan
a87e2293b7 résolution des conflits 2024-04-25 04:20:12 +02:00
Marwan
f1ff0628c4 je sais pas ce que je fais 2024-04-24 23:55:35 +02:00
0b241c72c4 -alpha: take one input separated by & 2024-04-16 14:24:06 +02:00
39ff2dbffc Add arguments to main.ml 2024-04-16 11:40:08 +02:00
5af7419020 Fix alpha renaming 2024-04-16 10:40:50 +02:00
bc697b30a0 Merge branch 2024-04-16 10:30:10 +02:00
d299e38fe0 Add alpha_equiv 2024-04-16 10:23:44 +02:00
Marwan
bd6dedc074 typage du exfalso, etc 2024-04-16 10:07:09 +02:00
Marwan
0b67d9a5eb types flèches et affichage des types 2024-04-15 12:07:49 +02:00
262f0364b7 Ajout du Makefile 2024-04-09 11:41:54 +02:00
8ba594ee3d Affichage des expressions 2024-04-09 11:30:52 +02:00
Marwan
e2e80bf55c initial commit 2024-04-09 11:09:33 +02:00