From aa68057c8581506a44f7eabc63725ea7f6fbbe40 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Mar 2022 05:18:27 -0700 Subject: [PATCH] chore: more general type universes in example --- tests/lean/run/deBruijn.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/deBruijn.lean b/tests/lean/run/deBruijn.lean index 5a82bd7b0b..85e9a39594 100644 --- a/tests/lean/run/deBruijn.lean +++ b/tests/lean/run/deBruijn.lean @@ -1,4 +1,4 @@ -inductive HList {α : Type u} (β : α → Type u) : List α → Type u +inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v) | nil : HList β [] | cons : β i → HList β is → HList β (i::is)