opencompl/lean-mlir-old

Issues

• Implement LLVM as an MLIR dialect

  #3 opened 2 years ago by bollu
  3

• Get rid of stale branches `match-matcher` and `linalg-semantics`

  #31 opened 2 years ago by lephe
  1

• Instcombine proofs that require lemmas

  #38 opened 2 years ago by bollu
  0

• Figure out how to use binport until Mathlib4 lands

  #46 opened 2 years ago by bollu
  1

• Check if p-adics can be use to simplify bitfiddling theory

  #51 opened 2 years ago by bollu
  0

• `TopM.get` always succeeds if dominance check passes

  #45 opened 2 years ago by bollu
  1

• Finish proof of rewriter

  #40 opened 2 years ago by bollu
  0

• Close linalg proofs with simple model

  #39 opened 2 years ago by bollu
  0

• C FFI

  #6 opened 2 years ago by bollu
  0

• Create data structures to navigate def/use chain

  #2 opened 2 years ago by bollu
  1

• Allow piping input for convenience

  #1 opened 2 years ago by bollu
  0

• Greedy Pattern rewriter

  #5 opened 2 years ago by bollu
  0

• Abstract interpretation

  #7 opened 2 years ago by bollu
  0

• Operational semantics

  #8 opened 2 years ago by bollu
  0

• Typed syntax

  #25 opened 2 years ago by lephe
  0

• Replace uses of P.lean / MLIRParser.lean with the EDSL

  #12 opened 2 years ago by lephe
  0

• Decidable type equality and finiteness of MLIRTy

  #10 opened 3 years ago by lephe
  1