From b912a4b36b85afbd959855b7ab3c5c1a88709dd3 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 3 Jan 2025 16:35:30 -0800 Subject: [PATCH] Make `lake build` work again --- LeanBoogie.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBoogie.lean b/LeanBoogie.lean index f6d0a58..5db31bf 100644 --- a/LeanBoogie.lean +++ b/LeanBoogie.lean @@ -1,4 +1,4 @@ -- This module serves as the root of the `LeanBoogie` library. -- Import modules here that should be built as part of the library. -import LeanBoogie.BoogieDsl +import LeanBoogie.Dsl