package main

type Bool enum {
    false
    true
}

type Maybe[A] enum {
    nothing Maybe[A]
    just(A) Maybe[A]
}

type Functor[F] class {
    fmap[A, B] :: (A -> B) -> F[A] -> F[B]
}

func (Maybe) Functor {
    fmap[A, B](f A -> B, x Maybe[A]) Maybe[B] {
        switch x {
        case nothing:
            return nothing[B]
        case just(a):
            return just[B](f(a))
        }
    }
}

func not(b Bool) Bool {
    switch b {
    case false:
        return true
    case true:
        return false
    }
}

@check Functor
@check fmap
@eval fmap(not, just true)
@eval fmap(not, nothing)

package main

type Nat enum {
    zero
    succ(Nat)
}

type Bool enum {
    false
    true
}

// Ask the compiler what the parameter is.
func isZero(n _) Bool {
    switch n {
    case zero:    return true
    case succ(k): return false
    }
}

// Two labelled holes, so the answers can be told apart.
func twice(n ?operand) ?result {
    return succ (succ n)
}

// A hole in a local, with something in scope around it.
func plusOne(n Nat) Nat {
    var m _ = succ n
    return m
}

holes-demo.ml:14:15: found hole '_' standing for Nat
holes-demo.ml:22:14: found hole '?operand' standing for Nat
holes-demo.ml:22:24: found hole '?result' standing for Nat
  in scope:
    n : Nat
holes-demo.ml:28:11: found hole '_' standing for Nat
  in scope:
    n : Nat

package main

@extern("fmt.Println")
func println(s String#) Unit#

@extern("os.Exit")
func exit(code GoInt#) Unit#

const greeting String# = "hello, world"

Definition Tiyin := Z.

Definition Percent := Z.

Definition pct (a : Tiyin) (p : Percent) : Tiyin :=
  Z.quot (a * p) 10000.