From df3129e80d136c488cec35d460623080cf3cd69a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2014 10:08:53 -0800 Subject: [PATCH] fix(library/hop_match): typo Signed-off-by: Leonardo de Moura --- src/library/hop_match.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/hop_match.h b/src/library/hop_match.h index ada6a9b39..089aac17c 100644 --- a/src/library/hop_match.h +++ b/src/library/hop_match.h @@ -21,7 +21,7 @@ namespace lean { We say non-free variables occurring in \c p and \c t are "locally bound". \c p is a higher-order pattern when in all applications in \c p - 1- A free variable is to the function OR + 1- A free variable is not the function OR 2- A free variable is the function, but all other arguments are distinct locally bound variables. \pre \c subst must be big enough to store all free variables occurring in subst