src/scenes/church_encoding.tsx


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
  Direction,
  beginSlide,
  createRef,
  slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";

const churchNumerals = [
  "0 = λ f . λ x . x (no application of f)",
  "1 = λ f . λ x . f x (one application of f)",
  "2 = λ f . λ x . f (f x) (two applications of f)",
  "succ = λ n . λ f . λ x . f ((n f) x)",
];

export default makeScene2D(function* (view) {
  const numerals = createRef<Txt>();

  view.add(
    <Layout layout direction="column" alignItems="center">
      <Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
        Church Encoding
      </Txt>
      <Txt
        ref={numerals}
        fontSize={30}
        fontFamily={theme.font}
        fill={theme.text.hex}
      ></Txt>
    </Layout>
  );

  yield* slideTransition(Direction.Right);
  yield* beginSlide("The Lambda Calculus - Church Encoding");

  for (const numeral of churchNumerals) {
    yield* numerals().text(numerals().text() + "\n\n" + numeral, 1);
    yield* beginSlide("substitution - " + numeral);
  }
});