config.toml

language = "untyped λ-calculus"
fragment = "pattern"

[[problems]]
constraints = [
    "∀ f: magic -> t, x: magic. X[f, x] = f Y[x]",
    "∀ x: magic. Y[x] = x x"
]

[[problems.solutions]]
name = "most general"
substitutions = [
    "Y[a: magic] ↦ a a",
    "X[b: magic -> t, c: magic] ↦ b (c c)",
]

[[problems.solutions]]
name = "with redundant substitution"
substitutions = [
    "Y[x: magic] ↦ x x",
    "X[f: magic -> t, x: magic] ↦ f (x x)",
    "M[x: t, y: t -> u] ↦ y x"
]

[[problems]]
constraints = [
    "∀ x:t. M[λy:t. x, λa:t. λa:t. a] = λy:t. x"
]

[[problems.solutions]]
name = "most general"
substitutions = [
    "M[a: t, b: t -> t] ↦ a",
]

[[problems]]
constraints = [
    "∀ x:t, y:t. M[λz:t.N[x, y], x y] = λa:t.λb:t.x"
]

[[problems.solutions]]
name = "some other solution"
substitutions = [
    "M[z1:t, z2:t] ↦ λa:t.z1",
    "N[z1:t, z2:t] ↦ z1"
]

[[problems]]
constraints = [
    "∀ x:t, y:t. M[λz:t.N[x, y], x] = λa:t.λb:t.x"
]

[[problems.solutions]]
name = "solution 1"
substitutions = [
    "M[z1:t, z2:t] ↦ λa:t.z1",
    "N[z1:t, z2:t] ↦ z1"
]

[[problems.solutions]]
name = "solution 2"
substitutions = [
    "M[z1:t, z2:t] ↦ λa:t.λb:t.z2",
]