Skip to content

Instantly share code, notes, and snippets.

@seankearon
Last active January 12, 2020 11:03
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Embed
What would you like to do?
Curry-Howard Exercise
// (A => B and not B) => not A
Not<A> ModusTollens<A, B>(
Func<A, B> A_implies_B,
Not<B> not_B)
{
Absurd A_to_Absurd(A a)
{
return not_B.Apply(A_implies_B(a));
}
return new Not<A>(A_to_Absurd);
}
// (A => B and B => C) => A => C
Func<A, C> Syllogism<A, B, C>(
Func<A, B> A_implies_B,
Func<B, C> B_implies_C)
{
C Composed(A a)
{
return B_implies_C(A_implies_B(a));
}
return Composed;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment