Search results

Intro top-of-stack does not support multiple arguments

Status: Open.

#18 In verse-lab/lean-ssr;

· dranov opened on Mar 7, 2024

Unexpected end of input

bugSomething isn't workingSomething isn't working

Status: Open.

#16 In verse-lab/lean-ssr;

· dranov opened on Mar 6, 2024

Error message when -> fails has the top of the stack as a hypothesis in the context

enhancementNew feature or requestNew feature or request

Status: Open.

#15 In verse-lab/lean-ssr;

· dranov opened on Mar 6, 2024

Code smell: kpattern and kpatternType are almost identical

Status: Open.

#14 In verse-lab/lean-ssr;

· dranov opened on Mar 6, 2024

Show correct proof state at end of line without requiring ;

enhancementNew feature or requestNew feature or request

Status: Open.

#13 In verse-lab/lean-ssr;

· dranov opened on Mar 6, 2024

Intro pattern equivalent of constructor

Status: Open.

#12 In verse-lab/lean-ssr;

· dranov opened on Mar 5, 2024

Eliminate/generalize terms, not just hypotheses

Status: Open.

#10 In verse-lab/lean-ssr;

· dranov opened on Mar 4, 2024

Sequence with case split

Status: Open.

#9 In verse-lab/lean-ssr;

· dranov opened on Mar 4, 2024

Look behind definitions (such that explicit unfolds are not needed) when performing rewrites

Status: Open.

#8 In verse-lab/lean-ssr;

· dranov opened on Mar 4, 2024

srw should rewrite everywhere in goal by default, not just first occurrence

Status: Open.

#7 In verse-lab/lean-ssr;

· dranov opened on Mar 4, 2024

Add support for custom induction principles

Status: Open.

#5 In verse-lab/lean-ssr;

· dranov opened on Mar 1, 2024

Add option to print standard Lean tactic script for SSR-Lean script

Status: Open.

#4 In verse-lab/lean-ssr;

· dranov opened on Mar 1, 2024