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.