From ca1e212d134eca2683404dd28e1d1edcab25bd9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 8 Aug 2024 16:57:38 +0200 Subject: [PATCH] Update src/Std/Sat/AIG/Basic.lean Co-authored-by: Markus Himmel --- src/Std/Sat/AIG/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) ""