Commit Graph
56 Commits
Author SHA1 Message Date
Adrien Vannson 97e0ead5fe Add spaces 2022-05-16 23:27:10 +02:00
Adrien Vannson e706c4bb9d Add comment 2022-05-16 23:25:49 +02:00
Adrien Vannson 7439ae817a Remove typecheck 2022-05-16 23:25:40 +02:00
Adrien Vannson b5cad5149c Merge branch 'master' of gitlab.aliens-lyon.fr:savrillo/pieuvre 2022-05-16 23:19:23 +02:00
Adrien Vannson 7aba10f5fc Typecheck 2022-05-16 23:19:18 +02:00
Mysaa 627214787e Ajout de Et, ou et des tests associés. 2022-05-16 04:01:23 +02:00
Mysaa 905b86af2d Correction de l'α-conversion. 2022-05-11 22:36:31 +02:00
Adrien Vannson 09ebe6339e Test d'alpha equivalence 2022-05-11 22:20:29 +02:00
Adrien Vannson 50e0046617 Merge branch 'master' of gitlab.aliens-lyon.fr:savrillo/pieuvre 2022-05-11 21:29:29 +02:00
Adrien Vannson f60d98ea78 Lecture de lambda-termes et reduce 2022-05-11 21:29:20 +02:00
Mysaa 92e1371027 Merge remote-tracking branch 'origin/master' 2022-05-10 15:25:38 +02:00
Mysaa 241a44528e Ajout de la β-réduction du λ-terme final. 2022-05-10 15:24:42 +02:00
Adrien Vannson 359d7333f5 Commentaire 2022-05-10 15:20:50 +02:00
Adrien Vannson 2ce406f7f2 Test 6 2022-05-10 15:15:59 +02:00
Adrien Vannson d451f1ba72 Test 1 2022-05-10 15:13:03 +02:00
Mysaa 98a9e6964f Merge remote-tracking branch 'origin/master' 2022-05-10 15:00:38 +02:00
Mysaa f1f890058f Merge branch 'cut' 2022-05-10 15:00:19 +02:00
Adrien Vannson 93e1174ff3 Renommage 2022-05-10 14:50:13 +02:00
Adrien Vannson dc29a93934 Affichage des subgoals 2022-05-10 14:44:07 +02:00
Adrien Vannson 5774bab7d8 Fonction find_hyp 2022-05-10 14:31:34 +02:00
Mysaa 2b98fd6407 Correction du typage de ExFalso. 2022-05-10 14:23:38 +02:00
Mysaa a1276102a7 Ajout du cut, un peu buggé pour l'instant. 2022-05-10 14:17:35 +02:00
Adrien Vannson 188bc43576 Modif d'un test 2022-05-10 14:15:18 +02:00
Adrien Vannson f6be1ad6da Test 8 2022-05-10 14:02:36 +02:00
Adrien Vannson 7eb605eb83 Test élimination du faux 2022-05-10 14:00:01 +02:00
Adrien Vannson e51762b03b Ajout de preuves 2022-05-10 13:57:02 +02:00
Adrien Vannson 07e7a6b4eb Text 2022-05-10 13:42:17 +02:00
Adrien Vannson 98d525c58a Elim 2022-05-10 13:41:20 +02:00
Adrien Vannson 4ca1a65529 Tests 2022-05-10 12:10:33 +02:00
Adrien Vannson 46fa8ce223 Merge branch 'master' of gitlab.aliens-lyon.fr:savrillo/pieuvre 2022-05-10 11:48:58 +02:00
Adrien Vannson 8fc318b75e Tests 2022-05-10 11:48:53 +02:00
Mysaa ed4471da44 Ajout du README 2022-05-10 11:25:25 +02:00
Adrien Vannson 29d7e67a00 Indentation 2022-05-10 11:23:09 +02:00
Mysaa 73984f4232 Merge remote-tracking branch 'origin/master' 2022-05-10 11:20:35 +02:00
Mysaa b13db5a7ba Ajout du typecheck des preuves finales. 2022-05-10 11:19:03 +02:00
Adrien Vannson 5af07fff8d Apply 2022-05-10 11:11:03 +02:00
Adrien Vannson b9d507b650 Ajout de tactic.ml 2022-05-10 10:31:30 +02:00
Adrien Vannson 40ac538cc1 Assumption 2022-05-09 00:42:33 +02:00
Adrien Vannson 5304002158 Affichage des hypothèses 2022-05-09 00:18:22 +02:00
Adrien Vannson 17907e1690 Construction du lambda-terme 2022-05-09 00:15:52 +02:00
Adrien Vannson ec7519ce98 Correction du parseur 2022-05-09 00:15:23 +02:00
Adrien Vannson 8f5488bf86 Suppression d'un warning 2022-05-08 22:37:54 +02:00
Adrien Vannson 5b7784184d Indentation 2022-05-08 22:34:25 +02:00
Adrien Vannson fc7317b2d0 Parse tactics 2022-05-08 20:03:29 +02:00
Adrien Vannson f833807253 Interractive mode 2022-05-08 18:52:04 +02:00
Adrien Vannson 34455d887d False 2022-05-08 18:29:54 +02:00
Adrien Vannson 136da4a898 Lecture de non 2022-05-08 18:18:36 +02:00
Adrien Vannson a5d820319a Correction d'un bug lors de la lecture de l'entrée standard 2022-05-08 18:14:13 +02:00
Adrien Vannson 15afcecabe Correction d'un bug 2022-05-08 18:10:08 +02:00
Adrien Vannson 4d6287f2cd Lecture d'une formule à prouver 2022-05-08 18:10:00 +02:00