diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index f979857d4873..9db44391f146 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -284,8 +284,8 @@ structure Entrypoint (α : Type) [DecidableEq α] [Hashable α] where /-- Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes. -/ -def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) - : String := +def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) : + String := let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry let (dag, s) := go "" decls hinv idx h |>.run .empty let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) ""