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

25 commits

Author SHA1 Message Date
Kim Morrison
4e0f6b8b45 feat: export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
Leonardo de Moura
27c79cb614
fix: double reset bug at ResetReuse (#4028) 
We conjecture this is the cause for the segfaults when compiling Mathlib
with #4006
 2024-04-29 23:26:07 +00:00
Henrik Böving
23e49eb519 perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Leonardo de Moura
3896244c55 chore: cleanup 2022-07-25 22:39:56 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Leonardo de Moura
2ebcf29cde chore: use a[i]! for array accesses that may panic 2022-07-02 15:12:05 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00
Leonardo de Moura
9d05023325 chore: remove some [specialize] annotations 2022-01-18 09:24:06 -08:00
Daniel Fabian
0238bf8c33 refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Leonardo de Moura
72a8fb84b5 feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
Leonardo de Moura
3b6d65c3c3 chore: use deriving Inhabited 2020-12-13 10:09:20 -08:00
Leonardo de Moura
f14826a730 fix: incorrect context used at addDecForDeadParams 2020-12-08 12:38:33 -08:00
Leonardo de Moura
2ebee8d00c fix: missing addJP 2020-12-08 12:09:52 -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
Leonardo de Moura
6858cb5fb6 chore: cleanup 2020-10-29 10:24:16 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
a915822454 chore: cleanup 2020-10-17 13:49:14 -07:00
Leonardo de Moura
73184bfe16 chore: move to new frontend 2020-10-16 16:30:55 -07:00
Leonardo de Moura
cbb14673ef chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Leonardo de Moura
249bda16c0 chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Leonardo de Moura
4ccc3fef52 chore: move Init.Lean files to Lean package 2020-05-26 15:04:35 -07:00
Renamed from src/Init/Lean/Compiler/IR/RC.lean (Browse further)