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
anda
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 typeVoid
- Tuples (desugaring to nested pairs)
- Dependent pair syntax
(x : T ** P x)
(there exists anx
of typeT
such thatP x
) - Inline
case
expressions - Heterogeneous equality
do
notation- Idiom brackets
- Type classes, supporting default methods and dependencies between methods
rewrite
prfin
expr- Metavariables
- Inline proof/tactic scripts
- Implicit coercion
codata
- Also
Inf : Type -> Type
type constructor for mixed data/codata. In factcodata
is implemented by putting recursive arguments underInf
. 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