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

331 commits

Author SHA1 Message Date
Leonardo de Moura
4dccaa963b feat: add List.mapTR and csimp lemma 2021-08-22 09:32:19 -07:00
Leonardo de Moura
ec6af1ba26 feat: use simple List.append definition and add csimp theorem 2021-08-21 16:11:54 -07:00
Leonardo de Moura
3b240d9a14 feat: use simple List.length definition and add csimp theorem 2021-08-21 13:11:06 -07:00
Leonardo de Moura
7066619123 refactor: define Nat.le using inductive type 2021-08-20 19:39:45 -07:00
Leonardo de Moura
a15a36b8d3 chore: cleanup Subarray instances 2021-08-13 19:29:09 -07:00
Leonardo de Moura
24fe2875c6 chore: change Pow class 
Based on the suggestion at https://github.com/leanprover/lean4/issues/433
 2021-08-12 13:59:55 -07:00
Leonardo de Moura
9cc94296e5 chore: remove staging workaround theorems 2021-08-07 12:52:31 -07:00
Leonardo de Moura
a821dcbff2 chore: enforce naming convention for theorems 
see issue #402

fix: `ElabTerm.lean`
 2021-08-07 12:48:38 -07:00
Leonardo de Moura
a230fe2d06 fix: forallMetaTelescope issue 
This commit incorporates the fix at PR #612, and clean up
`Meta/Basic.lean` using Lean 4 features.
 2021-08-06 09:47:10 -07:00
Wojciech Nawrocki
f1b4d9a193 chore: restore non-generic Format 
Motivation: it is unclear whether this is the best solution for embedding objects in pretty-printer outputs.
 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
b022a7c1d2 style: indent 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
9b8e44618d chore: default to Format Nat 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
a937fa26ba chore: fewer explicit types 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
f51b80060d feat: generic tagged Format 2021-08-01 09:58:44 +02:00
Leonardo de Moura
af5ff9ceb2 refactor: move List.takeWhile to Init.Data.List.Basic 
Motivation: make sure it will be aligned by BinPort
 2021-07-31 15:03:33 -07:00
Leonardo de Moura
f10c27dfb7 perf: add workaround for perf issue 
See issue #361
 2021-07-29 08:29:09 -07:00
Wojciech Nawrocki
776a0c71aa feat: add UInt64 unpackings 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
80d90038ad feat: add Format tags 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
caa8f7f7b2 chore: expose Substring.prev/next 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
7aca461a35 fix: hovers on elabFieldName fields 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
Wojciech Nawrocki
4ea3d2df2f feat: add missing UInt coercions 2021-07-05 19:42:01 +02:00
Leonardo de Moura
f4a7ffd8c8 chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Sebastian Ullrich
eb1e285e26 chore: style 2021-06-21 10:17:26 -07:00
Leonardo de Moura
e8a958d8f3 chore: parameter naming convention 2021-06-06 17:09:26 -07:00
Leonardo de Moura
37da993032 chore: remove HashableUSize instances 2021-06-02 08:48:11 -07:00
Leonardo de Moura
cbab9438c9 chore: Hashable instances for Expr and Level 2021-06-02 08:30:25 -07:00
Leonardo de Moura
5ac2e14173 chore: add Hashable that uses UInt64 2021-06-02 07:47:41 -07:00
Leonardo de Moura
43812444a7 chore: Hashable => HashableUSize 2021-06-02 07:24:26 -07:00
Leonardo de Moura
6a87bba9c0 chore: mixHash => mixUSizeHash 2021-06-02 07:05:42 -07:00
Sebastian Ullrich
3fb7a2c0e1 fix: make problematic Ord -> LT instance a def 2021-05-31 19:05:50 -07:00
François G. Dorais
29dc5c5b1b fix: duplicate namespace prefix 2021-05-31 13:31:57 +02:00
Sebastian Ullrich
693c2ccf71 feat: min, max, List.min/maximum? 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
37dcbf3421 feat: have Ord imply LT/LE 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
94aea76922 feat: FilePath.metadata 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
a02c6fd3eb chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Sebastian Ullrich
7c3101a51c chore: produce more efficient/pp-able array code from quotations 2021-05-19 09:52:35 +02:00
Leonardo de Moura
eae1f5412b fix: bugs introduced in the previous commits 2021-05-17 15:00:51 -07:00
Leonardo de Moura
3b7bcdc449 feat: add endPos field to SourceInfo.original 
We need an update stage0 before we use it.
 2021-05-17 14:32:58 -07:00
Leonardo de Moura
c7096f54a2 feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
Leonardo de Moura
8e81f03e3a chore: adjust stdlib to recent changes 2021-05-06 15:43:56 -07:00
Leonardo de Moura
7398db5f3f fix: rw final goal state 2021-05-04 16:58:44 -07:00
Sebastian Ullrich
aabb4a50aa feat: remove bracket-less rw 2021-05-04 15:24:22 -07:00
Leonardo de Moura
ba5d622e59 chore: avoid case tactic 2021-05-01 19:50:50 -07:00
Leonardo de Moura
920a2b2a14 perf: Ord USize instance and missing inline 2021-04-27 12:08:21 -07:00
Daniel Fabian
0238bf8c33 refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Leonardo de Moura
3a80e87793 chore: #405 step 1 2021-04-22 20:03:48 -07:00