Search results

Support <code>←</code> for <code>simp</code> rules

Status: Open.

#234 In leanprover-community/aesop;

· JLimperg opened on Jun 18, 2025

Rules for composite expressions need too many parentheses

Status: Open.

#233 In leanprover-community/aesop;

· JLimperg opened on Jun 18, 2025

Make <code>aesop</code> utilize <code>fin_cases</code>

Status: Open.

#232 In leanprover-community/aesop;

· madvorak opened on Jun 16, 2025

<code>aesop?</code> should not squeeze terminal <code>simp</code>

Status: Open.

#231 In leanprover-community/aesop;

· JLimperg opened on Jun 13, 2025

Partial <code>aesop?</code> should be able to close goals with unsafe rules

Status: Open.

#221 In leanprover-community/aesop;

· JLimperg opened on May 18, 2025

Tell Aesop to use a custom simp set

Status: Open.

#213 In leanprover-community/aesop;

· hgoldstein95 opened on Apr 10, 2025

Aesop search is nondeterministic in the proof state

Status: Open.

#211 In leanprover-community/aesop;

· eric-wieser opened on Apr 3, 2025

Create overnight version

Status: Open.

#202 In leanprover-community/aesop;

· madvorak opened on Mar 10, 2025

Use refined discrimination tree

Status: Open.

#198 In leanprover-community/aesop;

· JLimperg opened on Feb 26, 2025

Unfold Not in conclusions of forward rules?

Status: Open.

#197 In leanprover-community/aesop;

· JLimperg opened on Feb 26, 2025

Warning/error for constant forward rules

Status: Open.

#196 In leanprover-community/aesop;

· JLimperg opened on Feb 26, 2025

Allow <code>cases</code> on type definitions

Status: Open.

#193 In leanprover-community/aesop;

· JLimperg opened on Jan 31, 2025