fluoresce

Types

pub type Not(r, a) =
  fn(a) -> r
pub type NotNot(r, a) {
  Cont(run: fn(fn(a) -> r) -> r)
}

Constructors

  • Cont(run: fn(fn(a) -> r) -> r)
pub type Subtract(r, a, b) =
  #(a, Not(r, b))

Functions

pub fn adjunction(
  f: fn(fn(a) -> b) -> NotNot(b, c),
) -> NotNot(b, fn(fn(c) -> b) -> NotNot(b, a))
pub fn bind(
  c: NotNot(a, b),
  f: fn(b) -> NotNot(a, c),
) -> NotNot(a, c)
pub fn callcc(f: fn(fn(a) -> b) -> a) -> NotNot(b, a)
pub fn co(
  f: fn(fn(a) -> b) -> NotNot(b, c),
  rest: fn(Result(c, a)) -> NotNot(b, d),
) -> NotNot(b, d)
pub fn coexponential_to_function(
  c: fn(#(a, fn(b) -> c)) -> c,
) -> NotNot(c, fn(a) -> NotNot(c, b))
pub fn contramap(
  not_b: fn(a) -> b,
  f: fn(c) -> NotNot(b, a),
) -> NotNot(b, fn(c) -> b)
pub fn de_morgan_1(
  x: fn(Result(a, b)) -> c,
) -> NotNot(c, #(fn(b) -> c, fn(a) -> c))
pub fn de_morgan_2(
  x: #(fn(a) -> b, fn(c) -> b),
) -> NotNot(b, fn(Result(c, a)) -> b)
pub fn de_morgan_3(
  x: fn(#(a, b)) -> c,
) -> NotNot(c, Result(fn(b) -> c, fn(a) -> c))
pub fn de_morgan_4(
  x: Result(fn(a) -> b, fn(c) -> b),
) -> NotNot(b, fn(#(c, a)) -> b)
pub fn disjunctive_syllogism(
  e: NotNot(a, Result(b, c)),
  not_a: fn(c) -> a,
) -> NotNot(a, b)
pub fn do(c: NotNot(a, b), f: fn(b) -> c) -> NotNot(a, c)
pub fn double_negate(a: a) -> NotNot(b, fn(fn(a) -> b) -> b)
pub fn double_negation_elimination(
  not_not_a: fn(fn(a) -> b) -> b,
) -> NotNot(b, a)
pub fn excluded_middle() -> NotNot(a, Result(fn(b) -> a, b))
pub fn function_to_coexponential(
  f: fn(a) -> NotNot(b, c),
) -> NotNot(b, fn(#(a, fn(c) -> b)) -> b)
pub fn implies(
  f: fn(a) -> NotNot(b, c),
) -> NotNot(b, Result(c, fn(a) -> b))
pub fn join(a: NotNot(a, NotNot(a, b))) -> NotNot(a, b)
pub fn main() -> Int
pub fn modus_ponens(
  f: Result(a, fn(b) -> c),
  a: b,
) -> NotNot(c, a)
pub fn pierces_law(
  f: fn(fn(a) -> NotNot(b, c)) -> NotNot(b, a),
) -> NotNot(b, a)
pub fn throw(a: a, not_a: fn(a) -> b) -> NotNot(b, c)
pub fn wrap(a: a) -> NotNot(b, a)
Search Document