Combinatory Logic

Stream: Is there code for X?

[Becky T]

Greetings!
The combinators for the SKI combinatory calculus seem to have been removed in https://github.com/leanprover-community/mathlib4/pull/15188/files, and I do not know where they have been moved to.

A link to BCKW combinator calculus is also fine.

Trying to verify some manually abstracted terms, so I would like to be able to use reduce/rewriting tactics on the terms that I am testing, and Lean seems to have the nicest automation on this front.

Thank you in advance!

[Ruben Van de Velde]

They were moved to Mathlib/Deprecated/Combinator.lean in that pr, but I won't be surprised if they were removed entirely later. Probably they were deprecated because they're trivial and we didn't have any theorems about them

[Kevin Buzzard]

You can use the mathlib changelog to see when they were removed: https://mathlib-changelog.org/v4/def/Combinator.I

[Bhavik Mehta]

This doesn't quite answer your question, but I have this old file: https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166 which defines a number of useful things about SK combinators, and proves things about their reductions