From b2669610685b51422d0f45e7617086328cc81426 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Jan 2022 17:24:09 -0800 Subject: [PATCH] chore: fix test --- tests/lean/docStr.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index e768883fb7..680c7cb403 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -16,7 +16,7 @@ doc string for 'f' is not available doc string for 'g' is not available "let rec documentation at g " "Gadget for optional parameter support. " -"Auxiliary Declaration used to implement the named patterns `x@p`\n -- TODO: add proof for `x = a`\n" +"Auxiliary Declaration used to implement the named patterns `x@h:p` " "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\n it reduces `A` and continues bulding the telescope if it is a `forall`. " Foo := { range := { pos := { line := 4, column := 0 },