From d2956a902e449b691733d53708fad907f8c5875c Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 4 Mar 2024 22:15:16 +0100 Subject: [PATCH] fix: missing rename --- demo/Demo.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/demo/Demo.lean b/demo/Demo.lean index cf8ec02..19206f7 100644 --- a/demo/Demo.lean +++ b/demo/Demo.lean @@ -2,9 +2,9 @@ -- Import modules here that should be built as part of the library. import «Demo».Basic -import Subverso.Examples +import SubVerso.Examples -open Subverso.Examples +open SubVerso.Examples %example xdef def f (x : Nat) := %ex{add}{33 + %ex{X}{x}}