lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard
verified publisher icon opencompl

Executeable semantics for parametrized tests

Open goens opened this issue 1 year ago • 0 comments

Because of dependently-typed shenanigans, the executable semantics only work for concrete tests (with no mvars in the bitwidth). We should fix this.

goens avatar Feb 04 '24 16:02 goens