Violet

A small dependently typed language with inductive types, universe polymorphism, and user-defined operators.

curl -fsSL https://violet-lang.org/install.sh | sh

Quick start View on Codeberg

A taste of Violet

\universe 𝓤

\data Nat : 𝓤
  | 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)

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

Why Violet?

Inductive types

Define Nat, List, Vec, and equality with auto-generated eliminators.

Universe polymorphism

Write definitions once and reuse them across universe levels.

Stack-based syntax

Compose \elim, \intro, and \split to build clauses step by step.

User-defined operators

Declare infix operators with associativity and precedence, like + and *.

Records with eta

First-class record types with punning, update syntax, and definitional eta.

Modules

Top-level \import and \export; definitions are private by default.

Standard library

An MLTT standard library — Nat, List, Vec, Id, Bool, Σ — added as a git dependency with violet add.