Core Language Features — Idris 1.0 documentation

# 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`