Skip to content

Commit e2a8c8f

Browse files
Fix compilation warning
1 parent 4f9eafc commit e2a8c8f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

REPL/Util/Trie.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ and return the associated value, implemented iteratively to avoid stack overflow
103103
104104
Note the argument order is `(t s i)` to match usages in `Main.lean`.
105105
-/
106-
def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos) : Option α :=
106+
def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos.Raw) : Option α :=
107107
Id.run do
108108
let bytes := s.toUTF8
109109
let n := bytes.size

0 commit comments

Comments
 (0)