Search results

Add an option to pattern match using structural equality instead of definitional equality.

Status: Open.

#82 In leanprover-community/quote4;

· abdoo8080 opened on May 10, 2025

Example in README doesn't typecheck

Status: Open.

#57 In leanprover-community/quote4;

· fairflow opened on Sep 24, 2024

linter.constructorNameAsVariable false in turnExistsIntoForall

Status: Open.

#52 In leanprover-community/quote4;

· awalterschulze opened on Aug 23, 2024

assertInstancesCommute loops when there are several unnamed assumptions

Status: Open.

#38 In leanprover-community/quote4;

· dwrensha opened on Mar 7, 2024

Poor elaboration performance on structure matches

Status: Open.

#37 In leanprover-community/quote4;

· eric-wieser opened on Feb 20, 2024

<code>let mut</code> does not work with <code>~q</code> matching

bugSomething isn't workingSomething isn't working

Status: Open.

#36 In leanprover-community/quote4;

· eric-wieser opened on Feb 18, 2024

literal expressions not type-safe

Status: Open.

#34 In leanprover-community/quote4;

· ericrbg opened on Feb 7, 2024

invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables

Status: Open.

#30 In leanprover-community/quote4;

· eric-wieser opened on Dec 15, 2023

<code>~q</code> pattern match does not respect <code>return</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#21 In leanprover-community/quote4;

· Vtec234 opened on Aug 7, 2023

<code>foo.{$u}</code> is not supported

Status: Open.

#16 In leanprover-community/quote4;

· Vtec234 opened on Jun 27, 2023

Confusing type of <code>Expr</code> inputs in the local context

Status: Open.

#15 In leanprover-community/quote4;

· Vtec234 opened on Jun 26, 2023

Deep matching like Ltac's context

Status: Open.

#12 In leanprover-community/quote4;

· awalterschulze opened on Apr 28, 2023