WojciechKarpiel

#include <stdio.h>
#include <stdint.h>
typedef uint64_t calkowita;
typedef calkowita (fn)(void*,calkowita);

calkowita razy_n(void* dane, calkowita c){
  calkowita x = *((calkowita*) dane);
  return x*c;
}

WojciechKarpiel

public class DrzewoNaJawie {
    public static void main(String[] args){
        Drzewo d = new WęzełC(new WęzełA(0, 1), new WęzełB("xd"));
        System.out.println("Wynik: " + drzewoDoNapisu(d));
    }

    private static final Odwiedzacz<String> odwiedzaczNapisowy =
        new Odwiedzacz<String>(
                               a -> "[" + a.weźX() + ", " + a.weźY() + "]",
                               b -> "\"" + b.weźNapis() + "\"",

WojciechKarpiel

import core.cast.

module cedille-cast-07-08 (F: ★ ➔ ★) (mono : CastMap ·F).

--
Monotinic : (★ ➔ ★) ➔ ★ = λ F: ★ ➔ ★. CastMap ·F.
--

--alg
Alg : ★ ➔ ★ = λ X: ★. F ·X ➔ X.

WojciechKarpiel

module cedille-cast-05.

import core.top.
import data.sigma.
import data.sum.


NatF : ★ ➔ ★ = λ R: ★. Sum ·Top ·R. -- jenostka = 0; R = succ
ListF : ★ ➔ ★ ➔ ★ =  λ A : ★. λ R: ★. Pair ·Top ·R. -- jedn = nil; (a,r) = cons

WojciechKarpiel

module cedille-cast-04.

NatF ◂ ★ ➔ ★ = λ R: ★. ∀ X: ★. X ➔ (R ➔ X ➔ X) ➔ X.

zero-1 ◂ ∀ R: ★. NatF ·R = Λ R. Λ X. λ z. λ s. z.

zero-2 ◂ ∀ R: ★. NatF ·(NatF ·R) = Λ R. Λ X. λ z. λ s. z.

one-1 ◂ ∀ R: ★. NatF ·(NatF ·R)
  = Λ R. Λ X. λ z. λ s. s (zero-1 ·R) z.

WojciechKarpiel

module cedille-cast-01.

cNat ◂ ★ =  ∀ X: ★. X ➔ (X ➔ X) ➔ X.

czero ◂ cNat = Λ X. λ base. λ step. base.
csucc ◂ cNat ➔ cNat
  = λ n. Λ X. λ base. λ step. step (n base step).

iNat ◂ cNat ➔ ★
  = λ n: cNat. ∀ P: cNat ➔ ★. P czero ➔ (∀ m: cNat. P m ➔ P (csucc m)) ➔ P n.

WojciechKarpiel

\class Magma \extends BaseSet
  | \infixl 7 * : E -> E -> E

\class Monoid \extends Magma
  | ide : E
  | ide-left (x : E) : ide * x = x
  | ide-right (x : E) : x * ide = x
  | *-assoc (x y z : E) : (x * y) * z = x * (y * z)

-- Note that it does not extend Monoid