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

Commentaire

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-10 15:20:50 +02:00
parent 2ce406f7f2
commit 359d7333f5
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
main.ml
View File

@ -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;