issues
search
opencompl
/
lean-mlir
A minimal development of SSA theory
Other
88
stars
10
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
chore: prove that subtraction on BitStreams corresponds to subtraction on BitVectors
#559
AtticusKuhn
closed
2 months ago
23
Chore: Prove BitStream.neg_neg
#558
AtticusKuhn
closed
2 months ago
2
chore: avoid potentially unprotected raw literals
#557
tobiasgrosser
closed
2 months ago
1
[NFC] Chore: Canonicalise Bits of BitStream.addAux to match subAux and negAux
#556
AtticusKuhn
closed
2 months ago
14
feat: doz, max and min theorems
#555
AnotherAlexHere
closed
2 months ago
7
Chore: Prove that subtraction on BitVectors is the same as subtraction on BitStreams
#554
AtticusKuhn
closed
2 months ago
23
chore: drop two unused theorems
#553
tobiasgrosser
closed
2 months ago
1
chore: update to nightly-2024-08-17
#552
tobiasgrosser
closed
2 months ago
1
test: drop no_index
#551
tobiasgrosser
closed
2 months ago
1
chore: remove LLVM.intMin from ForLean
#550
tobiasgrosser
closed
2 months ago
1
chore: clean up toInt_pos_iff_[small|large] in forLean
#549
tobiasgrosser
closed
2 months ago
3
chore: drop unused theorem `toInt_eq'` from ForLean
#548
tobiasgrosser
closed
2 months ago
1
chore: canonicalize ForLean's `Nat` section
#547
tobiasgrosser
closed
2 months ago
2
chore: drop four theorems that are already upstream from forLean
#546
tobiasgrosser
closed
2 months ago
5
chore: update to 2024-08-16 tag
#545
tobiasgrosser
closed
2 months ago
1
chore: drop BitVec over constant value rewrites
#544
tobiasgrosser
closed
2 months ago
1
chore: move Nat theorems into namespace in ForLean
#543
tobiasgrosser
closed
2 months ago
1
chore: drop BitVec theorem already in lean
#542
tobiasgrosser
closed
2 months ago
1
chore: update to 2024-08-16
#541
tobiasgrosser
closed
2 months ago
2
chore: remove oldSectionVars in FHE
#540
goens
closed
2 months ago
5
chore: drop use of oldSectionVars from DCE
#539
tobiasgrosser
closed
2 months ago
3
chore: drop use of oldSectionVars from ErasedContext
#538
tobiasgrosser
closed
2 months ago
7
Chore: prove that addition on BitStreams corresponds to addition on BitVectors
#537
AtticusKuhn
closed
2 months ago
10
chore: drop unused import
#536
tobiasgrosser
closed
2 months ago
1
chore: remove `open Std (BitVec)`
#535
tobiasgrosser
closed
2 months ago
1
chore: remove unused monad theorems from Framework
#534
tobiasgrosser
closed
2 months ago
1
[NFC] Chore: Clean up "BitStream.lean" for Style
#533
AtticusKuhn
closed
2 months ago
3
chore: update to lean4:v4.11.0-rc2
#532
tobiasgrosser
closed
2 months ago
15
chore: fix non-terminal simp
#531
tobiasgrosser
closed
2 months ago
1
chose: clean up CSE
#530
tobiasgrosser
closed
2 months ago
2
chore: cleanup udiv lemmas
#529
tobiasgrosser
closed
2 months ago
1
chore: clean up a bit ForLean
#528
tobiasgrosser
closed
2 months ago
2
chore: cleanup BitVec.neg_neg proof in ForLean
#527
tobiasgrosser
closed
2 months ago
1
Chore: Add Documentation to Automata Tactic
#526
AtticusKuhn
closed
2 months ago
5
Handshake-DC: add support for Int in Streams
#525
luisacicolini
closed
2 months ago
13
chore: prove that negation on bitstreams is the same as negation on bitvectors
#524
AtticusKuhn
closed
2 months ago
59
Revert "chore: update to nightly-2024-08-08"
#523
tobiasgrosser
closed
2 months ago
1
chore: update to nightly-2024-08-08
#522
tobiasgrosser
closed
2 months ago
1
chore: clean up use of two_pow_pred_mod_two_pow in ForLean
#521
tobiasgrosser
closed
2 months ago
1
chore: cleanup Nat.*two_pow* theorems in ForLean
#520
tobiasgrosser
closed
2 months ago
1
chore: avoid non-terminal simp in ForLean
#519
tobiasgrosser
closed
2 months ago
1
chore: eliminate redundant BitVec.msb_one
#518
tobiasgrosser
closed
2 months ago
2
chore: remove unused lemma
#517
tobiasgrosser
closed
2 months ago
1
feat: add CI cache for tools
#516
tobiasgrosser
closed
2 months ago
1
chore: test CI speed with caching
#515
tobiasgrosser
closed
2 months ago
1
chore: test CI speed with caching
#514
tobiasgrosser
closed
2 months ago
1
feat: add CI to cache .lake directory
#513
tobiasgrosser
closed
2 months ago
2
chore: remove BitVec.getLsb_xor (already in lean)
#512
tobiasgrosser
closed
2 months ago
1
chore: remove lemma that is already in lean
#511
tobiasgrosser
closed
2 months ago
1
Chore: tactic alive_auto
#510
AnotherAlexHere
closed
2 months ago
4
Previous
Next