From d451f1ba72cd11c40fa5fc60ffc12ebdf94240bc Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 15:13:03 +0200 Subject: [PATCH 1/3] Test 1 --- tests/test01.8pus | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/test01.8pus b/tests/test01.8pus index 7a7c870..dedb199 100644 --- a/tests/test01.8pus +++ b/tests/test01.8pus @@ -2,4 +2,9 @@ intro f. intro b. intro a. -cut B -> C +cut B -> C. +intro g. +apply g. +assumption. +apply f. +assumption. From 2ce406f7f299f1b8ba1652e4645679aac1724059 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 15:15:59 +0200 Subject: [PATCH 2/3] Test 6 --- tests/test06.8pus | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tests/test06.8pus b/tests/test06.8pus index 58d5463..b391ab9 100644 --- a/tests/test06.8pus +++ b/tests/test06.8pus @@ -1 +1,11 @@ (A -> B -> C) -> (A -> B) -> A -> C +intro f. +intro g. +intro a. +cut B -> C. +intro h. +apply h. +apply g. +assumption. +apply f. +assumption. From 359d7333f50c90d91216392a9370acd41c19f1e5 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 10 May 2022 15:20:50 +0200 Subject: [PATCH 3/3] Commentaire --- main.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/main.ml b/main.ml index 31bc94e..94ea82f 100644 --- a/main.ml +++ b/main.ml @@ -148,11 +148,12 @@ while !subgoals <> [] do | None -> failwith ("Hypothesis " ^ var ^ " not found") | _ -> failwith ("Hypothesis " ^ var ^ " unusable") ) + (* Pour montrer A, on montre B -> A et B *) | Cut tint -> ( - subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals; - fill_holes := function - | (pf::px::s) -> f ((LApp(pf, px))::s) - | _ -> fail () + subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals; + fill_holes := function + | pf :: px :: s -> f ((LApp (pf, px)) :: s) + | _ -> fail () ) done;