From 3c519887d12f106963278348ec40de51bdd8ca6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Aug 2021 17:04:15 -0700 Subject: [PATCH] chore: generate error message when `MatchEqs` fail TODO: we currently do not generate equation theorems for `match` expressions using array literals. --- src/Lean/Meta/Match/MatchEqs.lean | 7 +------ tests/playground/matchEqs.lean | 4 ++-- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 5bb6d307fb..8f6cec745e 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -20,9 +20,6 @@ private def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do let args := lhs.getAppArgs if recVal.getMajorIdx >= args.size then failed let mut major := args[recVal.getMajorIdx] - if major.isAppOfArity ``Eq.symm 4 then - /- This is needed for supporting `CasesArraySizes.lean` used in the implementation of array literal matching. -/ - major := major.appArg! unless major.isFVar do failed return (← cases mvarId major.fvarId!).map fun s => s.mvarId else @@ -139,9 +136,7 @@ where else throwError "spliIf failed") <|> - (do trace[Meta.debug] "TODO\n{← ppGoal mvarId}" - -- TODO - admit mvarId) + (throwError "failed to generate equality theorems for `match` expression, support for array literals has not been implemented yet{MessageData.ofGoal mvarId}") prove (type : Expr) : MetaM Expr := withLCtx {} {} <| forallTelescope type fun ys target => do diff --git a/tests/playground/matchEqs.lean b/tests/playground/matchEqs.lean index 92d4c2b9b9..dd8a4d4125 100644 --- a/tests/playground/matchEqs.lean +++ b/tests/playground/matchEqs.lean @@ -42,7 +42,7 @@ def g (xs ys : Array Nat) : Nat := set_option trace.Meta.debug true set_option pp.proofs true --- set_option trace.Meta.debug true +-- set_option trace.Meta.debug truen test% f.match_1 test% h.match_1 -test% g.match_1 +-- test% g.match_1