What are the general forms for type ascription in Agda?

Background: I'm working through Prabakhar Ragde's "Logic and Computation Intertwined", a totally fantastic introduction to computational intuitionistic logic. In his last chapter, he walks through some basics using Agda. I've successfully installed Agda and managed to twist emacs' arm (it took a lot of arm-twisting!) to get agda-mode working fairly well, but I feel that I'm missing a summary of the various type ascription forms in Agda.

Specifically, working through a proof in Agda without my head exploding requires a fair amount of type ascription--Let's just say this has this type for now, okay?--and I find myself missing the ability to associate types with names in a uniform way. I now know about two ways of doing this, but I feel as though I'm missing a more general one.

Method 1: When using a "where" form, you can use a double-line specification to perform type ascription.
Method 2: When using an explicit lambda, I can use parens and a colon to ascribe a type to an identifier.

The following illustrates both of these (using definitions of or and negation that are simple but not included, sorry):

ex9 : ∀ (A B : Set) → ¬ (¬ (or A (¬ A)))
ex9 A B aornotaimpliesbottom = aornotaimpliesbottom (or-intro-2 nota)
  where nota : ¬ (A)
        nota = λ (a : A) → aornotaimpliesbottom (or-intro-1 a)

Method 1 is used to specify the type of nota, and method 2 is used to specify the type of nota's argument.

Here's the question, though: what if I want to use type ascription in an "expression" position? For instance, what if I wanted to specify the type of the term (or-intro-1 a) ? I could use a "where" clause to pull it out into its own binding, but .... ooh, actually, that doesn't seem to work; embedding a 'where' into a lambda is not working as expected. Oh! It looks like "let" works there. Okay, anyway, question remains: is there a lighter-weight way to specify the type of an expression inline?

Solution

You can define inline type annotation as follows:

infixl 0 _∋_
_∋_ : ∀{i}(A : Set i) → A → A
A ∋ x = x

Or import it from the standard library:

open import Function using (_∋_)

Then A ∋ exp works as an inline type annotation on any expression. For example, in your code as:

nota = λ (a : A) → aornotaimpliesbottom (or A (¬ A) ∋ or-intro-1 a)

You can also insert inline type annotation, or effectively query the type of an expression which is already in your code, by first inserting a hole like this:

nota = λ (a : A) → aornotaimpliesbottom (? ∋ or-intro-1 a)

Then hitting C-c-s while in the hole, which fills the hole using default inference.

It's also good to remember that let is syntactically more flexible than where. You can put let inside any expression, but where only works at binding scopes (at top level, immediately under module declarations, or immediately in function right hand sides).