Search results

Mismatch between trait and impl models with &mut in type parameter

Status: Open.

#961 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 29, 2026

Wrong binder for call to FnMut closure returning unit.

Status: Open.

#960 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 28, 2026

Wrong translation with slice update in tuple

Status: Open.

#938 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 15, 2026

Precompiled artifacts don't contain Lean shared libraries

Status: Open.

#937 In AeneasVerif/aeneas;

· joshlf opened on Apr 15, 2026

Could not match the contexts

Status: Open.

#930 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 13, 2026

Unsupported nested borrow

Status: Open.

#929 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 13, 2026

Extraction fails for closure with if-then-else and variable capture

Status: Open.

#924 In AeneasVerif/aeneas;

· abentkamp opened on Apr 9, 2026

Name clash between different impl methods

Status: Open.

#922 In AeneasVerif/aeneas;

· maximebuyse opened on Apr 9, 2026

scalar Eq generates = (Prop) instead of == (Bool) in Lean backend

Status: Open.

#920 In AeneasVerif/aeneas;

· oliver-butterley opened on Apr 8, 2026

Internal panic on zerocopy code (Hermes isValid annotation)

Status: Open.

#913 In AeneasVerif/aeneas;

· joshlf opened on Apr 4, 2026

Internal panic on zerocopy code (Hermes isSafe annotation)

Status: Open.

#912 In AeneasVerif/aeneas;

· joshlf opened on Apr 4, 2026

Ord instance for local type placed in Funs.lean but referenced from Types.lean

Status: Open.

#903 In AeneasVerif/aeneas;

· oliver-butterley opened on Apr 2, 2026