From 74f4316713ef6bb84c674d1f9b7073962634fd3a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 19 Aug 2024 11:01:11 +1000 Subject: [PATCH] coercion --- src/Init/Coe.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 4e6adaed0faa..bf40bf0b6c1b 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -313,6 +313,12 @@ instance optionCoe {α : Type u} : Coe α (Option α) where instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α where coe v := v.val +instance boolPredToPred : Coe (α → Bool) (α → Prop) where + coe r := fun a => Eq (r a) true + +instance boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where + coe r := fun a b => Eq (r a b) true + /-! # Coe bridge -/ /--