Skip to content

Commit

Permalink
fix: missing rename
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Mar 4, 2024
1 parent a6d9665 commit d2956a9
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions demo/Demo.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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}}
Expand Down

0 comments on commit d2956a9

Please sign in to comment.