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

fix: text ordering

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-08-03 18:10:39 -04:00 • committed by Leonardo de Moura
parent d116e2e923
commit fd3bf289c4
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/Widget/TaggedText.lean
View file

@ -120,7 +120,7 @@ where go (acc : String) : Array (TaggedText α) → String
| #[] => acc
| ts => match ts.back with
| text s => go (acc ++ s) ts.pop
| append as => go acc (ts.pop ++ as)
| append as => go acc (ts.pop ++ as.reverse)
| tag _ a => go acc (ts.set! (ts.size - 1) a)
end TaggedText