simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

more compressed output of equations

Browse source
This commit is contained in:
Simon Cruanes 2021-11-10 13:23:29 -05:00
parent f500704905
commit 0d00629923
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/base/Proof_quip.ml
View file

@ -130,12 +130,15 @@ end = struct
| PS.Step_view.Expr_eq { lhs; rhs } ->
add_needed_step lhs;
add_needed_step rhs;
let t = lazy (
let name = name_term lid in
let step = lazy (
let lhs = L_terms.find lhs
and rhs = L_terms.find rhs in
P.T.eq lhs rhs
let t = P.T.eq lhs rhs in
P.S_define_t_name (name, t)
) in
L_terms.add lid t
add_top_step step;
L_terms.add lid (lazy (P.T.ref name))
| PS.Step_view.Expr_bool {b} ->
let t = Lazy.from_val (P.T.bool b) in