From a31e0bc804c5ae26550de7251b38799bf78bab03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Katja=20Ber=C4=8Di=C4=8D?= Date: Thu, 16 May 2024 08:42:04 +0200 Subject: [PATCH] Rename the connected components certificate instance in LoadGraph --- LeanHoG/LoadGraph.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanHoG/LoadGraph.lean b/LeanHoG/LoadGraph.lean index 5df63f2..94662f4 100644 --- a/LeanHoG/LoadGraph.lean +++ b/LeanHoG/LoadGraph.lean @@ -47,7 +47,7 @@ unsafe def loadGraphAux (graphName : Name) (jsonData : JSONData) : Elab.Command. match jsonData.connectedComponents? with | .none => pure () | .some data => - let componentsCertificateName := certificateName graphName "CertificateI" + let componentsCertificateName := certificateName graphName "ConnectedComponentsCertificateI" let componentsCertificateQ : Q(ConnectedComponentsCertificate $graph) := connectedComponentsCertificateOfData graph data Elab.Command.liftCoreM <| addAndCompile <| .defnDecl { name := componentsCertificateName