Leonardo de Moura 2c5bafcbd8 fix: dead variables at match equation hypotheses ... This commit addresses an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structural.20Recursion.20Problem/near/284238723		2022-05-28 16:09:35 -07:00
..
Basic.lean	fix: pattern hover information	2022-04-08 15:03:42 -07:00
CaseArraySizes.lean	chore: remove arbitrary	2022-01-15 12:14:27 -08:00
CaseValues.lean	feat: add new flag to caseValues	2022-01-18 12:15:29 -08:00
Match.lean	chore: cleanup	2022-05-06 17:12:10 -07:00
MatchEqs.lean	fix: dead variables at match equation hypotheses	2022-05-28 16:09:35 -07:00
MatchEqsExt.lean	feat: improve match expression support at simp	2022-03-28 17:17:01 -07:00
MatcherInfo.lean	feat: match equation theorem generation for new h : discr notation encoding	2022-04-29 11:48:25 -07:00
MatchPatternAttr.lean	chore: cleanup	2020-10-27 13:26:21 -07:00
MVarRenaming.lean	chore: cleanup	2022-01-26 09:18:17 -08:00
Value.lean	feat: improve Match module for patterns containing Fin and UInt literals	2021-09-05 20:43:40 -07:00