diff --git a/MockMockingbird/Aviary.lean b/MockMockingbird/Aviary.lean index 44d20df..341640f 100644 --- a/MockMockingbird/Aviary.lean +++ b/MockMockingbird/Aviary.lean @@ -51,6 +51,13 @@ Cardinal -/ def C (x : α → β → δ) (y : β) (z : α) := x z y +/-- +Converse Warbler + +`W'xy = yxx` +-/ +def W' (x : α) (y : α → α → β) := y x x + /-- Dickcissel @@ -195,6 +202,13 @@ Robin -/ def R (x : α) (y : β → α → γ) (z : β) := y z x +/-- +Sage Bird + +`Θx = x(Θx)` +-/ +partial def Θ [Inhabited α] (x : α → α) := x (Θ x) + /-- Starling @@ -224,3 +238,10 @@ Vireo `Vxyz = zxy` -/ def V (x : α) (y : β) (z : α → β → γ) := z x y + +/-- +Warbler + +`Wxy = xyy` +-/ +def W (x : α → α → β) (y : α) := x y y diff --git a/MockMockingbird/Aviary.tex b/MockMockingbird/Aviary.tex index 011478e..6caba30 100644 --- a/MockMockingbird/Aviary.tex +++ b/MockMockingbird/Aviary.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{../../preamble} +\input{../preamble} \begin{document}