GitHub · Where software is built

Labels Milestones New issue

docgen should elide proof of lemmas (or make this an option)

#949

· alleystoughton opened

on Mar 23, 2026

pretty printing displays operators of the same name but different definitions the same

#928

· alleystoughton opened

on Mar 9, 2026

Improving the default pre-condition on `hoare` subgoals from `conseq` in pRHL

#925

· fdupress opened

on Mar 9, 2026

anomaly with incompatible rewriting in clones

#921

· alleystoughton opened

on Mar 2, 2026

Bug when trying to use a lemma from a section with clones

#920

· guilhemmizrahi-jpg opened

on Mar 2, 2026

SMT not using hypothesis

#918

· henriquejosefaria opened

on Feb 27, 2026

`case` could allow case analysis on goals whose head symbol is a `match` or `if`

#916

· fdupress opened

on Feb 27, 2026

Lemmas should allow explicit code

#902

· Gustavo2622 opened

on Feb 19, 2026

`proc change` does not allow to add code at the beginning of the prorgram.

#897

· strub opened

on Feb 12, 2026

Feedback on VSCode extension

#891

· mbbarbosa opened

on Feb 9, 2026

Allow rewriting below binders.

#864

· strub opened

on Jan 12, 2026

Make error messages from incorrect dependence on declared objects more actionable

#863

· oskgo opened

on Jan 12, 2026