Search results

[Suggestion] Rewrite rule: <code>List.any</code> with equality lambda to <code>List.elem</code>

Status: Open.

#100 In input-output-hk/Lean-blaster;

· felipeperet opened on Feb 26, 2026

Z3 process not killed when replacing <code>by blaster</code> with <code>sorry</code>

Status: Open.

#99 In input-output-hk/Lean-blaster;

· felipeperet opened on Feb 26, 2026

[Bug] Functional extensionality axiom has incorrect quantifier structure, causing unsoundness

area: smtSMT backend and solver integrationSMT backend and solver integration

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#97 In input-output-hk/Lean-blaster;

· felipeperet opened on Feb 25, 2026

[SPIKE] Ledger rules prototype for Blaster

enhancementNew feature or requestNew feature or request

Status: Open.

Task

#94 In input-output-hk/Lean-blaster;

· robpangilinanioi opened on Feb 16, 2026

Test cases for advanced Not normalization rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#90 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for Match elimination rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#89 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for arithmetic equality simplification rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#88 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for DIte factorization rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#87 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for ITE factorization rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#86 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for Dite to ite normalization rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#85 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for Int + Nat division and modulo simplification rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#84 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026

Test cases for projection propagation rules

area: optimizerExpression optimizationExpression optimization

area: testsTesting infrastructureTesting infrastructure

Status: Open.

#83 In input-output-hk/Lean-blaster;

· RSoulatIOHK opened on Jan 23, 2026