ST package:Agda
Strictification of Haskell code
argument will only be used in strictly positive position.
A rendering style. Allows us to specify constraints to choose among
the many different rendering options.
Strengthening substitution. First argument is
IMPOSSIBLE. In 'Strengthen err n ρ the number
n must be non-negative. This substitution should only be
applied to values t for which none of the variables
0 up to n - 1 are free in t[ρ], and in that
case n is subtracted from all free de Bruijn indices in
t[ρ]. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢
Strengthen n ρ : Δ, Θ @
The Elim is neutral and blocks a pattern match.
The code to lex string and character literals. Basically the same code
as in GHC.
Under at least one and only inductive constructors.
Attempt to unquote a serialized meta.
Strictly positive occurrence.