guard package:Agda
guardConstraint c blocker tries to solve blocker
first. If successful without constraints, it moves on to solve
c, otherwise it adds a c to the constraint pool,
blocked by the problem generated by blocker.
guardPointerEquality x y s m behaves as
m if
x and
y are equal as pointers, or does nothing
otherwise. Use with care, see the documentation for
unsafeComparePointers
Like
guard, but raise given error when condition fails.
Translates guard alternatives to if-then-else cascades.
The builtin translation must be run before this transformation.
The current guardedness level.
Would termination go through with guardedness?
Guardedness does not help with termination.
Guardedness would provide termination evidence.
Guarded strictly positive occurrence (i.e., under ∞). For checking
recursive records.
Binds no variables
The guard must only use the variable that the case expression matches
on.