From ce64629d63d4d0c3cc182b29ea84c8ce62200108 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 29 Jul 2021 15:04:22 -0700 Subject: [PATCH] chore: two comments about bad pp.analyze behavior --- tests/lean/hidingInaccessibleNames.lean | 2 +- tests/lean/parserPrio.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/lean/hidingInaccessibleNames.lean b/tests/lean/hidingInaccessibleNames.lean index ee590f1edc..fffa3cbb52 100644 --- a/tests/lean/hidingInaccessibleNames.lean +++ b/tests/lean/hidingInaccessibleNames.lean @@ -5,7 +5,7 @@ def f : (xs : List Nat) → Nat → xs ≠ [] → Nat set_option pp.inaccessibleNames true in def f' : (xs : List Nat) → Nat → xs ≠ [] → Nat - | [], _, _ => _ + | [], _, _ => _ -- TODO: figure out why hyp `Ne (α := List Nat) x✝² []` needs α | [a,b], _, _ => _ | _, _, _ => _ diff --git a/tests/lean/parserPrio.lean b/tests/lean/parserPrio.lean index 371e4a06d2..1f3c99ec52 100644 --- a/tests/lean/parserPrio.lean +++ b/tests/lean/parserPrio.lean @@ -23,6 +23,8 @@ syntax (name := mySingleton) "[" term "]" : term macro_rules (kind := mySingleton) | `([$a]) => `(2 * $a) +-- TODO: "ambiguous, possible interpretations" error messages print with +-- a lot of detail since most mvars have not been resolved yet #check [1] -- ambiguous it can be `mySingleton` or the singleton list