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

dbg

Browse source
This commit is contained in:
Simon Cruanes 2021-03-30 16:00:36 -04:00
parent 903243643f
commit 7b2b11486f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/th-data/Sidekick_th_data.ml
View file

@ -235,7 +235,7 @@ module Make(A : ARG) : S with module A = A = struct
let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = let merge cc n1 c1 n2 c2 e_n1_n2 : _ result =
Log.debugf 5 Log.debugf 5
(fun k->k "(@[%s.merge@ (@[:c1 %a %a@])@ (@[:c2 %a %a@])@])" (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])"
name N.pp n1 pp c1 N.pp n2 pp c2); name N.pp n1 pp c1 N.pp n2 pp c2);
(* build full explanation of why the constructor terms are equal *) (* build full explanation of why the constructor terms are equal *)
(* TODO: have a sort of lemma (injectivity) here to justify this in the proof *) (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *)