From 542a998f0ece3782d0f978bd4a0287ab33d8bdf1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Sep 2015 09:46:51 -0700 Subject: [PATCH] fix(tests/lean): adjust tests to reflect changes in the HoTT library --- tests/lean/626b.hlean | 2 +- tests/lean/hott/614.hlean | 2 +- tests/lean/hott/615.hlean | 2 +- tests/lean/hott/ind_tac4.hlean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/lean/626b.hlean b/tests/lean/626b.hlean index 993e4c37b..4ab5956ae 100644 --- a/tests/lean/626b.hlean +++ b/tests/lean/626b.hlean @@ -1,4 +1,4 @@ -import hit.circle +import homotopy.circle open circle definition f (x : S¹) : bool := circle.rec_on x _ _ diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean index bd3521479..075fb966a 100644 --- a/tests/lean/hott/614.hlean +++ b/tests/lean/hott/614.hlean @@ -1,4 +1,4 @@ -import hit.circle +import homotopy.circle open circle eq int pi diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean index 74c5d0c1a..021003ab5 100644 --- a/tests/lean/hott/615.hlean +++ b/tests/lean/hott/615.hlean @@ -1,5 +1,5 @@ -- HoTT -import hit.circle +import homotopy.circle open circle eq int pi attribute circle.rec circle.elim [recursor 4] diff --git a/tests/lean/hott/ind_tac4.hlean b/tests/lean/hott/ind_tac4.hlean index b35a6f49d..55c33a007 100644 --- a/tests/lean/hott/ind_tac4.hlean +++ b/tests/lean/hott/ind_tac4.hlean @@ -1,4 +1,4 @@ -import hit.circle +import homotopy.circle open circle attribute circle.elim_on [recursor 2]