Skip to content

issues Search Results · repo:leanprover-community/aesop language:Lean

Filter by

71 results
 (48 ms)

71 results

inleanprover-community/aesop (press backspace or delete to remove)

leanprover-community/aesop
Use refined discrimination tree

We should use Jovan Gerbscheid s refined discrimination tree to improve the precision of indexing when rules contain functions. This would likely make a massive difference for measurability and continuity, ...
  • JLimperg
  • Opened 
    10 days ago
  • #198

leanprover-community/aesop
Unfold Not in conclusions of forward rules?

The forward rule @[aesop safe destruct] theorem not_prime_one : ¬Prime 1 (taken from Mathlib) currently means that in any context, ¬Prime 1 should be added as a hypothesis. But it was perhaps intended ...
  • JLimperg
  • 1
  • Opened 
    10 days ago
  • #197

leanprover-community/aesop
Warning/error for constant forward rules

Forward rules with no premises (or, more precisely, no slots) are supported, but are rarely useful and more likely to be tagged by mistake, so we should warn. Destruct rules with no slots should be an ...
  • JLimperg
  • Opened 
    10 days ago
  • #196

leanprover-community/aesop
Allow `cases` on type definitions

When a type definition unfolds to an application of an inductive type (e.g. def T := Bool), it should be possible to have @[aesop cases] T.
  • JLimperg
  • Opened 
    on Jan 31
  • #193

leanprover-community/aesop
Penalise unsafe rules that assign mvars

We currently penalise safe rules that assign mvars with a 10% lower success probability. However, the same penalty is not applied to unsafe rules, leading to some weird behaviour. See here.
  • JLimperg
  • Opened 
    on Jan 21
  • #191

leanprover-community/aesop
Try weaker variant of `simp_all`

Aesop uses simp_all by default. This rewrites with equations from the context, which can cause issues when the equations are not properly oriented. We could instead try to use a weakened variant of simp_all ...
  • JLimperg
  • 1
  • Opened 
    on Jan 14
  • #190

leanprover-community/aesop
Adding certain rules causes kernel error in later theorem

I m not 100% sure this is an Aesop problem, it could be a core Lean issue, but I can t get the issue to happen without Aesop so I m starting here. Here s an example of a couple of very simple theorems: ...
  • hgoldstein95
  • Opened 
    on Dec 27, 2024
  • #186

leanprover-community/aesop
bug: unexpected `sorry` usage

After updating the version of Aesop, sorry is now used in proofs that used to pass without sorry. Below is the code to reproduce the problem. import Aesop abbrev Variable := String def State := Variable ...
  • Seasawher
  • 2
  • Opened 
    on Nov 12, 2024
  • #177

leanprover-community/aesop
Linter for inductive/structure rules

Most rule builders should warn when applied to an inductive or structure. 99% of the time this is a mistake. Use case at leanprover-community/mathlib4#17810.
  • JLimperg
  • Opened 
    on Oct 28, 2024
  • #172

leanprover-community/aesop
Success probability sometimes increases for child goals

Here is a case where a child goal is assigned a greater success probability than its parent. Copying may be to blame.
  • JLimperg
  • Opened 
    on Oct 28, 2024
  • #171
Issue origami icon

Learn how you can use GitHub Issues to plan and track your work.

Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub Issues
ProTip! 
Press the
/
key to activate the search input again and adjust your query.
Issue origami icon

Learn how you can use GitHub Issues to plan and track your work.

Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub Issues
ProTip! 
Press the
/
key to activate the search input again and adjust your query.
Issue search results · GitHub