付録A 構文早見表

let x: i64 := 10
var y: i64 := 1
y := y + 1

fn add(a: i64, b: i64): i64 { a + b }
let larger := if x > y { x } else { y }
perform show("larger", larger)

・ add

larger = 10

shared struct Pair2(A: Shared, B: Shared) { first: A, second: B }
shared enum Choice(A: Shared) { None2, Some2(A) }
let p := Pair2 { first: 3, second: "ok" }
perform show("first", p.first)

first = 3

import std::prelude::Affine

fn read(&v: Vec(i64)): u64 { Vec::len(&v) }

fn write(&mut v: Vec(i64)): () {
  Vec::push(&mut v, 1)
}

var v := Vec::new()
write(&mut v)
perform show("n", read(&v))

・ read
・ write

n = 1

import std::Base

effect choose(): i64 resume ω

let out := handle { perform choose() } with {
  choose(), k => k(1) + k(2)
  return v => v
}
perform show("out", out)

theorem id_prop(P: Prop, p: P): P { p }
theorem equal(n: Nat): n = n { Refl }

✓ theorem id_prop : ∀ P: Prop. (P) -> P
✓ theorem equal : ∀ n: Nat. n = n

out = 3