l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix partial match

Browse Source
This commit is contained in:
augustin64 2024-05-14 10:49:24 +02:00
parent 52ecb564fb
commit 215c51758d
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
main.ml
View File

@ -60,7 +60,11 @@ let alpha_get_lam where_from =
- g, gs : next goals - g, gs : next goals
- sq : previous states of the interactive loop - sq : previous states of the interactive loop
*) *)
let rec interactive ((cg, (g, gs))::sq : (interactive_state) list) : proof = let rec interactive (sl : (interactive_state) list) : proof =
let (cg, (g, gs)), sq = match sl with
[] -> (None, (None, [])), []
| s::sq -> s, sq
in
begin begin
let _ = match g with let _ = match g with
None -> print_string "\n\027[1mNo more goals.\027[0m\n" None -> print_string "\n\027[1mNo more goals.\027[0m\n"
@ -85,6 +89,9 @@ let rec interactive ((cg, (g, gs))::sq : (interactive_state) list) : proof =
interactive [None, (None, [])] interactive [None, (None, [])]
end else begin end else begin
print_error "Typing failed" ""; print_error "Typing failed" "";
(* print_expr l;
print_newline ();
print_ty t; *)
(cg, (g, gs))::sq |> interactive (cg, (g, gs))::sq |> interactive
end end
end end