Skip to content

Commit 492f3b4

Browse files
committed
chore: make Subrelation reducible
1 parent 38b4062 commit 492f3b4

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Core.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1330,7 +1330,7 @@ def emptyRelation {α : Sort u} (_ _ : α) : Prop :=
13301330
`Subrelation q r` means that `q ⊆ r` or `∀ x y, q x y → r x y`.
13311331
It is the analogue of the subset relation on relations.
13321332
-/
1333-
def Subrelation {α : Sort u} (q r : α → α → Prop) :=
1333+
@[reducible] def Subrelation {α : Sort u} (q r : α → α → Prop) :=
13341334
∀ {x y}, q x y → r x y
13351335

13361336
/--

0 commit comments

Comments
 (0)