michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(builtin/heq): remove unnecessary import

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-17 15:40:56 -08:00
parent 70828af6db
commit ba88a3b05a
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/builtin/heq.lean
View file

@ -1,5 +1,3 @@
import macros
-- Heterogenous equality -- Heterogenous equality
variable heq {A B : TypeU} : A → B → Bool variable heq {A B : TypeU} : A → B → Bool
infixl 50 == : heq infixl 50 == : heq