Skip to content

Commit

Permalink
fix: PrefixTree WellFormed type
Browse files Browse the repository at this point in the history
`β` is a parameter.
  • Loading branch information
leodemoura committed Mar 6, 2022
1 parent 1450a86 commit b105c00
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Data/PrefixTree.lean
Expand Up @@ -64,7 +64,7 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α
| some t => find ks t d
find k t init

inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
inductive WellFormed {β} (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
| emptyWff : WellFormed cmp empty
| insertWff {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val)

Expand Down

0 comments on commit b105c00

Please sign in to comment.