From 6d03a9383a697da51d3e8e6b8a28bd0ee3c92e34 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 2 May 2023 10:34:47 -0600 Subject: [PATCH] Add additional recursive, non immediately-duplicative birds. --- MockMockingbird/Aviary.lean | 21 +++++++++++++++++++++ MockMockingbird/Aviary.tex | 2 +- 2 files changed, 22 insertions(+), 1 deletion(-) 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}