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

fix(library/init/meta/relation_tactics): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-29 07:25:58 +01:00
parent 3963fa7cad
commit 75eab6471d
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/relation_tactics.lean
View file

@ -15,7 +15,7 @@ do tgt ← target,
r ← return $ get_app_fn tgt,
match op_for env (const_name r) with
| some refl := mk_const refl >>= apply
| none := fail (tac_name ++ " tactic failed, target is not a reflexive relation application")
| none := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
end
meta_definition reflexivity : tactic unit :=