search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

Remove toNat from LLVM semantics #699

Closed lfrenot closed 2 weeks ago

lfrenot commented 2 weeks ago

This closes: https://github.com/opencompl/lean-mlir/issues/694

lfrenot commented 2 weeks ago

It would probably be nice if someone who actually knows lean/lean-mlir to go through the changes to the proofs I made

To see if there aren't easier/better ways to do them

github-actions[bot] commented 2 weeks ago

Alive Statistics: 76 / 93 (17 failed)

github-actions[bot] commented 2 weeks ago

Alive Statistics: 76 / 93 (17 failed)