diff --git a/main.ml b/main.ml index ef7c7ef..85d51cd 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; 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. 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.