From d56db0a22dcc867f08930c07aed0b7270ce2cdf1 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 2 Aug 2021 13:19:51 -0700 Subject: [PATCH] doc: pp.analyze one more comment about a failure --- tests/lean/run/PPTopDownAnalyze.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 01d3f824ea..5ce0fc80c0 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -336,3 +336,7 @@ set_option pp.notation false in -- TODO: this error occurs because it cannot solve the universe constraints -- (unclear if it is too few or too many annotations) -- #testDelabN ExceptT.seqRight_eq + +-- TODO: this error occurs because a function has explicit binders while its type has +-- implicit binders. This may be an issue in the elaborator. +-- #testDelabN Char.eqOfVeq