From d68665f7a2d30333fc2e4af503de1e9d19bfc3fc Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sun, 23 Jul 2017 09:48:08 +0100 Subject: [PATCH] chore(library/init/meta/tactic): fix copy-paste error in docstring --- library/init/meta/tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 906f1d5ebc..291a962855 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -385,7 +385,7 @@ meta constant get_univ_assignment : level → tactic level /-- Return the value assigned to the given meta-variable. Fail if argument is not a meta-variable or if it is not assigned. -/ meta constant get_assignment : expr → tactic expr -/-- Return the value assigned to the given meta-variable. +/-- Return true if the given meta-variable is assigned. Fail if argument is not a meta-variable. -/ meta constant is_assigned : expr → tactic bool meta constant mk_fresh_name : tactic name