max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26363 commits 1 branch 0 tags 5.3 GiB
Commit graph

40 commits

Author SHA1 Message Date
Sebastian Ullrich
978e94272c feat: String.replace 2021-11-18 09:42:35 +01:00
Wojciech Nawrocki
bc8027cdc6 perf: speed up String.intercalate 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
caa8f7f7b2 chore: expose Substring.prev/next 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
b2d712a766 fix: Substring.splitOn 2021-07-19 09:55:37 +02:00
Daniel Fabian
93a3fd14ad refactor: do not use explicit instance, but use deriving instead. 2021-07-13 09:58:27 -07:00
Daniel Fabian
0d41fd03f7 feat: add xml parser. 
in order to generate the LLVM extern declarations we want to use a generator that spits out XML. Hence adding a small XML parser.
 2021-07-13 09:58:27 -07:00
Leonardo de Moura
f4a7ffd8c8 chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Leonardo de Moura
e8a958d8f3 chore: parameter naming convention 2021-06-06 17:09:26 -07:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00
Leonardo de Moura
3a80e87793 chore: #405 step 1 2021-04-22 20:03:48 -07:00
Leonardo de Moura
e8401ea6e7 chore: remove old instances 2021-01-20 18:12:35 -08:00
Sebastian Ullrich
79107a2316 feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
8ad061e328 feat: leanpkg: change print-path to print-paths that also emit LEAN_SRC_PATH (unused as of yet) 2021-01-19 19:06:01 +01:00
Sebastian Ullrich
d7733ba662 feat: use leanpkg print-path for worker initialization 2021-01-19 19:06:01 +01:00
Wojciech Nawrocki
af04c66e22 chore: comment style in Init.String.Basic 2021-01-15 13:29:22 -08:00
Wojciech Nawrocki
f3ab908888 fix: substring APIs 2021-01-15 13:29:22 -08:00
Sebastian Ullrich
1f563695bb feat: From/ToJson derive handlers 2020-12-26 19:38:24 +01:00
Leonardo de Moura
76fb1799fe chore: goodies for deriving command 2020-12-11 18:08:50 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
d6f778bec4 refactor: arbitrary without explicit arguments 
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
 2020-11-25 09:07:38 -08:00
Sebastian Ullrich
cf9a2ae6af feat: formatter: preserve comments 2020-11-25 11:30:24 +01:00
Leonardo de Moura
f3779f1542 feat: add support for unbound implicit locals 2020-11-20 12:22:27 -08:00
Leonardo de Moura
304c80d610 feat: use <| 2020-11-19 09:03:38 -08:00
Leonardo de Moura
9c9d65e640 chore: move definitions needed by macros to Prelude.lean 2020-11-11 06:56:45 -08:00
Leonardo de Moura
cca3bad0bb feat: add Prelude.lean 
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
 2020-11-10 18:08:18 -08:00
Leonardo de Moura
2daeb195b5 chore: use new names 2020-11-10 10:15:19 -08:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes 
closes #203
 2020-10-27 18:29:19 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
30ce419e06 chore: move to new frontend 2020-10-23 12:14:34 -07:00
Leonardo de Moura
de66ca3943 feat: add helper functions for writing macros 2020-10-23 10:59:59 -07:00
Wojciech Nawrocki
bbcc718c8d chore: more server fixes 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
7b9363c828 refactor: simplify document storage in server 2020-08-31 06:50:01 -07:00
Sebastian Ullrich
b2714d36ef fix: String: take/drop characters, not bytes 2020-08-11 18:24:47 -07:00
Sebastian Ullrich
c5d226ba36 feat: HasBeq for Syntax, Substring 2020-08-06 09:26:49 -07:00
Leonardo de Moura
12c5075c67 fix: String.dropRight 2020-03-23 14:51:05 -07:00
Leonardo de Moura
41949ee801 refactor: String.toNat ==> String.toNat? and String.toNat! 2020-03-23 14:29:48 -07:00
Leonardo de Moura
364bb7bdf7 fix: proper Name literals 
cc @kha
 2020-01-24 12:38:15 -08:00
Simon Hudon
6d8927da10 fix: little details 2020-01-12 08:02:48 -08:00
Leonardo de Moura
2809cea147 chore: remove DecidableEq workaround 
We have better indexing now.
 2019-11-26 17:30:18 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -08:00
Renamed from library/Init/Data/String/Basic.lean (Browse further)