Core Language Features
- Full-spectrum dependent types
- Strict evaluation (plus
Lazy : Type -> Type
type constructor for
explicit laziness)
- Lambda, Pi (forall), Let bindings
- Pattern matching definitions
- Export modifiers
public
, abstract
, private
- Function options
partial
, total
where
clauses
- “magic with”
- Implicit arguments (in top level types)
- “Bound” implicit arguments
{n : Nat} -> {a : Type} -> Vect n a
- “Unbound” implicit arguments —
Vect n a
is equivalent to the
above in a type, n
and a
are implicitly bound. This applies
to names beginning with a lower case letter in an argument position.
- ‘Tactic’ implicit arguments, which are solved by running a tactic
script or giving a default argument, rather than by unification.
- Unit type
()
, empty type Void
- Tuples (desugaring to nested pairs)
- Dependent pair syntax
(x : T ** P x)
(there exists an x
of
type T
such that P x
)
- Inline
case
expressions
- Heterogeneous equality
do
notation
- Idiom brackets
- Interfaces (like type classes), supporting default methods and dependencies between
methods
rewrite
prf in
expr
- Metavariables
- Inline proof/tactic scripts
- Implicit coercion
codata
- Also
Inf : Type -> Type
type constructor for mixed data/codata.
In fact codata
is implemented by putting recursive arguments under
Inf
.
syntax
rules for defining pattern and term syntactic sugar
- these are used in the standard library to define
if ... then ... else
expressions and an Agda-style preorder
reasoning syntax.
- Uniqueness
typing
using the
UniqueType
universe.
- Partial
evaluation
by
%static
argument annotations.
- Error message reflection
- Eliminators
- Label types
'name
%logging n
%unifyLog