Go backward to Semantics of Type Declarations Go up to Top Go forward to Array Indexing

Declarations

D: Declaration -> Environment -> Store ->
    (Environment x Poststore)
D[[D₁; D₂]] = lambda e.lambda s.
    let (e', p') = (D[[D₁]]e s)
    in (check (D[[D₂]]e'))(p)
D[[var I:T]] = lambda e.lambda s.
    let (d, p) = T[[T]]s
    in ((updateenv [[I]] d e), p)

A declaration activates the storage allocation strategy specified by its type structure.