Function Declarations
Functions are the primary building blocks for organizing code in Sector9. This page covers the basic func syntax, parameters, return types, body forms, and where verification contracts attach.
Anonymous Functions
Anonymous functions (also called lambda expressions or function literals) create inline function values without declaring a named function. They are essential for callbacks, quantifiers, and higher-order programming.
Higher-Order Functions
Higher-order functions take other functions as parameters or return functions as results. They enable abstractions like map, filter, and fold patterns, but in verification mode every function value must be pure or have a contract type.
Generic Functions
Generic functions use type parameters to write code that works with any type. Instead of writing separate functions for Int, Bool, and Nat, you write one function parameterized by ``. The verifier specializes each used instantiation, so contracts stay attached to the concrete version that is called.