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

chore(library/init/meta/tactic): fix copy-paste error in docstring

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-23 09:48:08 +01:00
parent 25aa847aba
commit d68665f7a2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/tactic.lean
View file

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