Search results

Compiling Lean files breaks the CI

Status: Open.

#569 In AeneasVerif/aeneas;

· sonmarcho opened on Jul 4, 2025

Support for Sized

Status: Open.

#551 In AeneasVerif/aeneas;

· dylanede opened on Jun 17, 2025

Fix the goto definition for the theorems generated by the macros <code>uscalar</code>, <code>iscalar</code>, etc.

Status: Open.

#547 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 16, 2025

<code>scalar_tac</code> simplifies the goal *then* saturates it

Status: Open.

#540 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 11, 2025

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

Status: Open.

#539 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 11, 2025

Make <code>scalar_tac_preprocess</code> unfold the reducible definitions

Status: Open.

#537 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 10, 2025

Namespaces in generated Lean code

Status: Open.

#536 In AeneasVerif/aeneas;

· dylanede opened on Jun 6, 2025

Automatically generate the tutorial exercises from the solutions

Status: Open.

#534 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 5, 2025

Universe polymorphism in Lean backend

Status: Open.

#533 In AeneasVerif/aeneas;

· dylanede opened on Jun 5, 2025

<code>progress</code> fails on some goals

Status: Open.

#532 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 4, 2025

Incorrect extraction on loop with copy

Status: Open.

#500 In AeneasVerif/aeneas;

· ayhon opened on Apr 13, 2025

<code>eval_global</code> fails on <code>usize</code> and <code>isize</code> expressions.

Status: Open.

#492 In AeneasVerif/aeneas;

· ayhon opened on Apr 9, 2025