Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master'

Browse Source
This commit is contained in:
Mysaa 2022-05-10 15:25:38 +02:00
commit 92e1371027
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
3 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
main.ml
View File

@ -148,11 +148,12 @@ while !subgoals <> [] do
| None -> failwith ("Hypothesis " ^ var ^ " not found") | None -> failwith ("Hypothesis " ^ var ^ " not found")
| _ -> failwith ("Hypothesis " ^ var ^ " unusable") | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
) )
(* Pour montrer A, on montre B -> A et B *)
| Cut tint -> ( | Cut tint -> (
subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals; subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
fill_holes := function fill_holes := function
| (pf::px::s) -> f ((LApp(pf, px))::s) | pf :: px :: s -> f ((LApp (pf, px)) :: s)
| _ -> fail () | _ -> fail ()
) )
done; done;

7
tests/test01.8pus
View File

@ -2,4 +2,9 @@
intro f. intro f.
intro b. intro b.
intro a. intro a.
cut B -> C cut B -> C.
intro g.
apply g.
assumption.
apply f.
assumption.

10
tests/test06.8pus
View File

@ -1 +1,11 @@
(A -> B -> C) -> (A -> B) -> A -> C (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.