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.