Search results

Add lemmas for <code>x[i]</code>

Status: Open.

#665 In AeneasVerif/aeneas;

· sonmarcho opened on Dec 3, 2025

<code>simp_scalar</code> doesn't close a goal

Status: Open.

#654 In AeneasVerif/aeneas;

· sonmarcho opened on Nov 26, 2025

Invalid generation of names and patterns

Status: Open.

#652 In AeneasVerif/aeneas;

· sonmarcho opened on Nov 25, 2025

Add UScalar.xor_spec to Lean backend

Status: Open.

#649 In AeneasVerif/aeneas;

· hatoo opened on Nov 25, 2025

could you bump the version to 4.25.0-rc2 (current mathlib one)?

Status: Open.

#634 In AeneasVerif/aeneas;

· alok opened on Nov 13, 2025

The file <code>tests/lean/lakefile.lean</code> is regerenated in the Lean CI, but not tested for diff

Status: Open.

#623 In AeneasVerif/aeneas;

· sonmarcho opened on Oct 20, 2025

Implement a <code>bvify by</code> tactic

Status: Open.

#621 In AeneasVerif/aeneas;

· sonmarcho opened on Oct 9, 2025

Bug: disjoint borrows in a slice

Status: Open.

#615 In AeneasVerif/aeneas;

· Nadrieril opened on Oct 1, 2025

Bug with <code>scalar_tac</code>

Status: Open.

#614 In AeneasVerif/aeneas;

· sonmarcho opened on Sep 30, 2025

Use notations like <code>+?</code>, <code>-?</code>, etc. for scalar binops which can fail

Status: Open.

#613 In AeneasVerif/aeneas;

· sonmarcho opened on Sep 30, 2025

<code>make setup-charon</code> fails with <code>error[E0554]: #![feature] may not be used on the stable release channel</code>

Status: Open.

#603 In AeneasVerif/aeneas;

· kim-em opened on Sep 3, 2025

Internal error in option.rs

Status: Open.

#576 In AeneasVerif/aeneas;

· UlrikBuchholtz opened on Jul 13, 2025