Expand description
Verification error types with Socratic error messages.
§Philosophy
Errors in this module follow the Socratic method: they guide users toward understanding rather than simply reporting failures. Each error type includes:
- A clear description of what went wrong
- Context about why it matters
- Guidance on how to address the issue
- When available, a concrete counterexample
§Error Categories
| Category | Error Types | User Action |
|---|---|---|
| Logic | ContradictoryAssertion, BoundsViolation, RefinementViolation | Fix the logical issue |
| License | LicenseRequired, LicenseInvalid, LicenseInsufficientPlan | Provide valid license |
| Solver | SolverUnknown, SolverError | Simplify or restructure |
| Termination | TerminationViolation | Add decreasing variant |
Structs§
- Counter
Example - A counterexample showing concrete values that falsify an assertion.
- Verification
Error - A verification error with Socratic explanation.
Enums§
- Verification
Error Kind - The category of verification error.
Type Aliases§
- Verification
Result - Result type for verification operations.