From ac4961fa374d3ed443f3fdcd0a0ef540a21f91f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Jan 2021 07:36:16 -0800 Subject: [PATCH] test: check stdlib doc strings --- tests/lean/docStr.lean | 3 +++ tests/lean/docStr.lean.expected.out | 3 +++ 2 files changed, 6 insertions(+) diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean index f4fd62ad3a..053420b33d 100644 --- a/tests/lean/docStr.lean +++ b/tests/lean/docStr.lean @@ -67,5 +67,8 @@ def printDocStrings : MetaM Unit := do printDocString `f.foo printDocString `g printDocString `g.foo + printDocString `optParam + printDocString `namedPattern + printDocString `Lean.Meta.forallTelescopeReducing #eval printDocStrings diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index 181d35bc24..bdf600b41e 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -15,3 +15,6 @@ doc string for 'f' is not available "let rec documentation at f " 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` " +"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`. "