 Syntax and concepts
 Sugar
This is an extremely quick explanation of Agda,
a proof editor I have used based on constructive type theory.
A precursor of Agda was CHalf, now obsolete.
Agda is written in haskell and emacs lisp, and is quite easy to
use. The editing
interface is a standard emacs mode, which is a front end for a
line mode interpreter. It is a simple and elegant tool for carefully
working out definitions and constructive proofs.
Thomas Hallgren in Chalmers has written an editing GUI called
alfa, which
provides an alternative, sexier environment for proof editing. It
also is quite easy to use, though it requires a powerful machine.
There are other developments connected with Agda; eg. seemingly
something written by Aarne
Ranta that will translate proofs into ordinary natural languages.
Syntax and concepts
In Agda one has:
 Functions

 functional types:
 (x :: A)> B
 abstraction form:
 \ (x :: A)> b
 application form:
 b a
 Named products

 product form:
 sig { x1 :: A1; .. }
 tuple form:
 struct { x1=a1; .. }
 selection form:
 a.xi
These let you chunkup blocks
of formal material, and refer to chunk components by name. Note:
the blocks can be empty, as in sig{},struct{}.
 Named sums

 sum form:
 data { x1 ( y1 : A1, .. , yk : Ak )  .. } .
Here the xi are constructor names, that live in a name space
specific to each instance of the type. Constructors are
disambiguated as follows
xi@type
.
 constructor form:
 x1 a1 .. ak
 case form:
 case a of { (x1 y1 .. yk) > a1 ; .. }
Facilities for tagging data with named
constructors. Note: there can be zero tags data{}; and a given
tag may have no data data{..,$xi,..}. The behaviour of constructors
with respect to typechecking is extremely subtle. They exhibit a
kind of polymorphism; they are not functions.
 Lets
 let { x1 :: A1 = a1, .. } in a
Definitions can be mutually recursive.
 Sets, Types, Kind, Packages
 Set : Type : Kind, Theory : Kind
 Set, Type, and Kind
are (predicatively) closed under the above constructions.
Packages are named collections of definitions whose definitions take
the form package name params where { x1 =
a1 : A1, .. } , and the definitions within them may be selected
by name as with tuples. Packages are supplemented with a lot of
useful sugar, which I havent got time to describe just now.
Sugar
There is a certain amount of extra sugar that goes with these.
Here is some (I may have forgotten something).
 layout
 Very usefull: one can use layout (indentation) instead of syntactical noise
like braces, semicolons, etc.
 Infix operators
 A name may be used as an infix operator,
by enclosing it in backquotes, as in
`foo`
.
 Symbolic operators
 I haven't mastered these.
 repeated abstraction form:
 \ (x,y::A) > a is sugar for
\ (x :: A) > \ (y :: A) > a .
 repeated functional form:
 ( x, y : A, .. ) > a is sugar for
( x :: A ) > (y :: A)> .. > a .
 left hand side parameters:

f ( x1 :: A1, .. ) :: A = a is sugar for
f = (x1 :: A1) > .. A = \ (x1 :: A1) .. > a : ( x1 : A1, .. )> A
 use of `useless variables'

In ( x : A )> B, the variable x need'nt occur in B.
It's a drag to think of a name. Instead, one may use
(in binding position) the identifier "_", as in Haskell. This usually helps to
make the code clearer.
If a name is supplied it is used by the
proof editor as a default, when one sends the checker an Intro
command.
Furthermore, there's the familar abbreviation
A > B
of (_ :: A) > B
.
Nestable comments in Agda are like this { .. }.
One line comments (to end of line) are introduced by 
.
Files may be included with special comments
#include "file.name"
Unfinished bits are represented like this: {! text !} or ?
.
Sometime I might try to describe what it is the typechecker does.