coercion

leanprover · Aug 19, 2024 · 5ef7407 · 5ef7407
1 parent b486c67
commit 5ef7407
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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 -/
 
 /--