diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 64fed7f58..5bc638247 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -1,5 +1,3 @@ -import macros - -- Heterogenous equality variable heq {A B : TypeU} : A → B → Bool infixl 50 == : heq