max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Data
History
Jon Eugster 3dd811f9ad
chore: remove FileMap.lines and add FileMap.getLine (#3237) 
`FileMap.lines` is an array that seems to be manually managed to have
the form `#[1, 2, ..., n-1, n-1]` with same length as
`FileMap.positions`. Remove this structure field in favour of
calculating the line number as `min(x+1, positions.size-1)` when needed.

Follow-up on #3221
2024-03-25 10:33:04 +00:00
..
Json chore: revert ToJson/FromJson Sum (#3759) (#3760) 2024-03-25 09:09:44 +00:00
Lsp feat: diagnostics for stale dependencies (#3247) 2024-03-18 10:38:38 +00:00
Xml chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00
Array.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
AssocList.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Format.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
FuzzyMatching.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
HashMap.lean feat: allow duplicate theorems to be imported 2024-03-13 12:57:41 -07:00
HashSet.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Json.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
JsonRpc.lean feat: snapshot trees and language processors (#3014) 2024-03-14 13:40:08 +00:00
KVMap.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LBool.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LOption.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Lsp.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Name.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
NameMap.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
NameTrie.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
OpenDecl.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Options.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Parsec.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PersistentArray.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PersistentHashMap.lean refactor: clean up public API around Array.eraseIdx (#3676) 2024-03-17 06:25:10 +00:00
PersistentHashSet.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Position.lean chore: remove FileMap.lines and add FileMap.getLine (#3237) 2024-03-25 10:33:04 +00:00
PrefixTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Rat.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
RBMap.lean chore: upstream solve_by_elim (#3408) 2024-02-21 01:16:04 +00:00
RBTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SMap.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SSet.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Trie.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Xml.lean chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00