simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-24 18:36:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

quip: add clause in expr_def

Browse source
This commit is contained in:
Simon Cruanes 2021-11-10 18:04:52 -05:00
parent 0d00629923
commit 8c780e3ed5
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/base/Proof_quip.ml
View file

@ -170,12 +170,21 @@ end = struct
add_needed_step c;
add_needed_step rhs;
let name = name_clause lid in
let step = lazy (
(* add [name := (|- c=rhs) by refl c].
Make sure we do it first, order in final proof will be reversed. *)
let step_refl = lazy (
let c = L_terms.find c in
let rhs = L_terms.find rhs in
P.S_step_c {name; res=[P.Lit.eq c rhs]; proof=P.refl c}
) in
add_top_step step_refl;
(* define [c:=rhs] *)
let step_def = lazy (
let c = L_terms.find c in
let rhs = L_terms.find rhs in
P.S_define_t (c, rhs)
) in
add_top_step step;
add_top_step step_def;
L_proofs.add lid (lazy (P.ref_by_name name));
| PS.Step_view.Expr_not { f } ->