Search results

Add missing InBounds/Fields lemmas for <code>BlockPtr.setArguments</code>

Status: Open.

#137 In opencompl/veir;

· math-fehr opened on Jan 22, 2026

Make sure our <code>simp</code> can trigger

Status: Open.

#136 In opencompl/veir;

· math-fehr opened on Jan 21, 2026

Figure out wether to use <code>BlockOperand</code> or <code>Successor</code>

Status: Open.

#135 In opencompl/veir;

· math-fehr opened on Jan 21, 2026

Handle escape sequences in string literals in MLIR parser

Status: Open.

#107 In opencompl/veir;

· math-fehr opened on Jan 14, 2026

Implement ByteArray.Slice and use it in the lexer and parser

Status: Open.

#104 In opencompl/veir;

· math-fehr opened on Jan 13, 2026

Tracking of GetSet and Well-Formed lemmas

Status: Open.

#49 In opencompl/veir;

· math-fehr opened on Dec 21, 2025

Remove <code>missingOps</code> from <code>BlockPtr.OpChain</code>

Status: Open.

#47 In opencompl/veir;

· math-fehr opened on Dec 21, 2025

Do not have both pointers and structure in WellFormed structure

Status: Open.

#44 In opencompl/veir;

· math-fehr opened on Dec 20, 2025

Rationalize theorem names

Status: Open.

#29 In opencompl/veir;

· ineol opened on Dec 17, 2025

Run Mathlib linters

Status: Open.

#12 In opencompl/veir;

· ineol opened on Dec 10, 2025