max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/run/coroutine): abbreviate abbreviation

Browse source
This commit is contained in:
Sebastian Ullrich 2019-08-09 11:04:02 +02:00
parent 934054b8d0
commit 8f55517d8c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/coroutine.lean
View file

@ -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