Creates a (not qualified) Agda variable name from a String.

Create a qualified identifier given a local identifier as Name and a list of module Names.

Creates a qualified name using an empty list of module names.

Creates an open import declaration for the given qualified name.

open import [modName]

Smart constructor for creating a module containing a list of declarations.

Smart constructor for creating function type declarations.

funcSig foo expr = foo : expr

Smart constructor for pattern synonyms.

pattern C x₁ … xₙ = pure (c x₁ … xₙ)

Smart constructor for function definitions.

f a₁ … aₙ = expr

Creates an application AST node in a pattern context.

Application is left associative. Parenthesis are added automatically if the right child is also an AppP node.

e a

Creates an integer literal.

Creates a string literal.

Creates a lambda expression, binding the given names and abstracting the given expression.

λ x y … → [expr]

Creates an application AST node.

Application is left associative and in type expressions binds stronger than type arrow. For these cases paren- thesis are added automatically.

e a

Applies the list of arguments to the given expression. If the expression is an operator the application is written in mixfix notation.

Helper function for creating expressions from Strings.

Hides the given expression.

e ↦ {e}

if_then_else_ from the base library.

cond true false ↦ if cond then true else false

case_of_ from the base library.

disrc clauses ↦ case disrc of λ { clause₁ ; clause₂ ; … }

Smart constructor for a clause of a pattern matching lambda abstraction.

Each LamClause stores a pattern matched on the left-hand side of an → and the expression on the right-hand side. In Agda lambda expressions can pattern match on their arguments.

The first level of Agda's hierarchy of type theoretic universes.

Creates a data declaration with the given name, binding the list of type variables and defining the list of constructors.

D [b₁, …, bₙ] [C₁, …, Cₘ]
  ↧
data D b₁ … bₙ : Set where
  C₁
  ⋮
  Cₘ

Creates a binder with visible args.

[α₁, …, αₙ] e ↦ (α₁ … αₙ : e)

A smart constructor for non dependent function types.

Creates a pi type binding the given names as hidden variables.

pi [α₁, …, αₙ] expr ↦ ∀ {α₁} … {αₙ} → expr