Structures

Struct definitions are proposition-level constraints that describe product values. Struct values are runtime data.

def Person : prop := struct
  name : str
  age : int

The compiler generates a constructor and field projectors:

def person : Person := Person.mk "Alice" 30
def name : str := Person.name person
def age : int := Person.age person

When the expected constraint is known, a named-field literal is also available:

def other : Person := {name := "Bob", age := 28}

Struct methods

A definition whose first explicit parameter is a struct value can be called with receiver notation:

def greet (person : Person) : str := "Hello, " + person.name

def message : str := (Person.mk "Alice" 30).greet

Currying lets the receiver bind the first argument while later arguments remain:

def greet_for (person : Person) (punctuation : str) : str :=
  "Hello, " + person.name + punctuation

def greet_alice : str -> str := (Person.mk "Alice" 30).greet_for

Struct definitions are erased after checking; struct values and their field access remain in generated C.