| Copyright | (c) Iago Abal, 2012 (c) David Castro, 2012 |
|---|---|
| License | BSD3 |
| Maintainer | Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> |
| Safe Haskell | None |
| Language | Haskell98 |
Z3.Lang.Nat
Description
- data Nat
Documentation
This type allows to reason about natural numbers.
Naturals are just integers plus a (>= 0) invariant, and we ensure that
this invariant is always preserved by transparently adding new assertions
to the context.
Note that arithmetic on naturals must result in natural numbers, otherwise the problem becomes unsatisfiable.