| 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
Deprecated: The Z3.Lang interface will be moved to a dedicated package.
- 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.