Examples

A short tour through some real Violet programs.

Natural numbers and addition

\export Nat add

\data Nat : U
  | zero : Nat
  | suc : Nat -> Nat

\let add : (m n : Nat) -> Nat \where
  add m n <= \elim m
  | add zero n => n
  | add (suc m) n => suc (add m n)

Length-indexed vectors

\import nat

\export Vec

\data Vec (A : U) : Nat -> U
  | nil : Vec A zero
  | cons : {n : Nat} -> A -> Vec A n -> Vec A (Nat/suc n)

Propositional equality

\export Id sym trans cong subst

\data Id {A : U} (x : A) : A -> U
  | refl : Id x x

\operator "~x = ~y" => Id x y
  \associativity: \left

# Symmetry: x = y implies y = x.
\let sym {A : U} {x y : A} : x = y -> y = x \where
  sym p <= \elim p
  | sym refl => refl

Records with punning

\record Point : U
  | x : Nat
  | y : Nat

\let origin : Point => { x = Nat/zero, y = Nat/zero }

# { x, y } desugars to { x = x, y = y }
\let pt (x : Nat) (y : Nat) : Point => { x, y }

User-defined operators

\operator "~x + ~y" => add
  \associativity: \left

\operator "~x * ~y" => mul
  \stronger_than: +
  \associativity: \left