Search results

declaration has metavariables error with matching and recursion

Status: Open.

#126 In leanprover-community/quote4;

· vasnesterov opened on Jan 27, 2026

misc/examples.lean currently PANICs

Status: Open.

#105 In leanprover-community/quote4;

· kim-em opened on Sep 24, 2025

Incorrect highlighting with variables

Status: Open.

#98 In leanprover-community/quote4;

· Vtec234 opened on Aug 20, 2025

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

let mut does not work with ~q 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

~q pattern match does not respect return

bugSomething isn't workingSomething isn't working

Status: Open.

#21 In leanprover-community/quote4;

· Vtec234 opened on Aug 7, 2023