Adrien Vannson
|
2d6028e010
|
Style
|
2022-05-19 21:50:57 +02:00 |
|
Adrien Vannson
|
819ce2d6de
|
Petites modifs
|
2022-05-18 16:44:34 +02:00 |
|
Adrien Vannson
|
d631cd3e93
|
Intros
|
2022-05-18 16:36:02 +02:00 |
|
|
|
d8f791328d
|
Ajout de True et de la tactique exact.
|
2022-05-18 00:53:01 +02:00 |
|
Adrien Vannson
|
a03a5f5504
|
log.8pus
|
2022-05-17 12:08:25 +02:00 |
|
|
|
b3d949f764
|
Merge remote-tracking branch 'origin/master'
|
2022-05-17 11:34:04 +02:00 |
|
|
|
dcd0b8f2d4
|
Ajout des jolies erreur et correction de la β-reduction.
|
2022-05-17 11:33:12 +02:00 |
|
Adrien Vannson
|
425951b1b9
|
Typecheck
|
2022-05-17 11:23:54 +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 |
|
|
|
627214787e
|
Ajout de Et, ou et des tests associés.
|
2022-05-16 04:01:23 +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 |
|
|
|
92e1371027
|
Merge remote-tracking branch 'origin/master'
|
2022-05-10 15:25:38 +02:00 |
|
|
|
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 |
|
|
|
98a9e6964f
|
Merge remote-tracking branch 'origin/master'
|
2022-05-10 15:00:38 +02:00 |
|
|
|
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 |
|
|
|
a1276102a7
|
Ajout du cut, un peu buggé pour l'instant.
|
2022-05-10 14:17:35 +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
|
29d7e67a00
|
Indentation
|
2022-05-10 11:23:09 +02:00 |
|
|
|
73984f4232
|
Merge remote-tracking branch 'origin/master'
|
2022-05-10 11:20:35 +02:00 |
|
|
|
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
|
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
|
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
|
a5d820319a
|
Correction d'un bug lors de la lecture de l'entrée standard
|
2022-05-08 18:14:13 +02:00 |
|
Adrien Vannson
|
4d6287f2cd
|
Lecture d'une formule à prouver
|
2022-05-08 18:10:00 +02:00 |
|
|
|
19a4354c66
|
Ajout de l'α-conversion et des fonctions d'affichage des λ-termes et des types.
|
2022-05-03 15:13:58 +02:00 |
|
|
|
1d760b1565
|
Ajout des types et des fonctions à implémenter.
|
2022-05-03 12:00:36 +02:00 |
|
|
|
107cef8edd
|
Premier commit - Structure des fichiers
|
2022-05-03 10:34:31 +02:00 |
|
