max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: PrefixTree WellFormed type

Browse source 
`β` is a parameter.
This commit is contained in:
Leonardo de Moura 2022-03-06 07:30:34 -08:00
parent 1450a86c4d
commit b105c006a5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Data/PrefixTree.lean
View file

@ -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)