max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: pp.analyze one more comment about a failure

Browse source
This commit is contained in:
Daniel Selsam 2021-08-02 13:19:51 -07:00 • committed by Sebastian Ullrich
parent 2afc18323d
commit d56db0a22d
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -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