From 8f55517d8c83f4ff86ceffdbc962c82badf39a3e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 9 Aug 2019 11:04:02 +0200 Subject: [PATCH] chore(tests/lean/run/coroutine): abbreviate `abbreviation` --- tests/lean/run/coroutine.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index fabd2fca3e..071e82724e 100644 --- a/tests/lean/run/coroutine.lean +++ b/tests/lean/run/coroutine.lean @@ -17,7 +17,7 @@ inductive coroutineResultCore (coroutine : Type (max u v w)) (α : Type u) (δ : inductive coroutine (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) | mk {} : (α → coroutineResultCore coroutine α δ β) → coroutine -abbreviation coroutineResult (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) := +abbrev coroutineResult (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) := coroutineResultCore (coroutine α δ β) α δ β namespace coroutine