From 194247f75b7617db1fc8e080d3101960a04d58a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Nov 2014 14:59:03 -0800 Subject: [PATCH] refactor(library/logic/wf): minimize dependencies --- library/logic/wf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/logic/wf.lean b/library/logic/wf.lean index 6af3b2db1..4063bdb42 100644 --- a/library/logic/wf.lean +++ b/library/logic/wf.lean @@ -1,7 +1,7 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura -import logic +import logic.eq inductive acc {A : Type} (R : A → A → Prop) : A → Prop := intro : ∀x, (∀ y, R y x → acc R y) → acc R x