From 726a5547de68d96338a6a21a7b7bebe5865edd70 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 10 Apr 2018 14:18:31 +0200 Subject: [PATCH] fix(init/core): typed_expr should accept Props Fixes #1954 --- library/init/core.lean | 2 +- tests/lean/run/1954.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1954.lean diff --git a/library/init/core.lean b/library/init/core.lean index a1c1528c58..ecbe11f678 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -105,7 +105,7 @@ a @[reducible] def out_param (α : Sort u) : Sort u := α /-- Auxiliary declaration used to implement the notation (a : α) -/ -@[reducible] def typed_expr (α : Type u) (a : α) : α := a +@[reducible] def typed_expr (α : Sort u) (a : α) : α := a /- id_rhs is an auxiliary declaration used in the equation compiler to address performance diff --git a/tests/lean/run/1954.lean b/tests/lean/run/1954.lean new file mode 100644 index 0000000000..e9e000a563 --- /dev/null +++ b/tests/lean/run/1954.lean @@ -0,0 +1,2 @@ +def all (p : ℕ → Prop) : Prop := ∀x, p x +example {p : ℕ → Prop} (h : all p) : p 0 := ‹all p› 0