Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
inox
Manage
Activity
Members
Labels
Plan
Issues
0
Issue boards
Milestones
Wiki
Code
Merge requests
6
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LARA
inox
Commits
7ea0c1c1
Commit
7ea0c1c1
authored
8 years ago
by
Nicolas Voirol
Committed by
GitHub
8 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Create tutorial.md
parent
b0afaf48
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/doc/tutorial.md
+42
-0
42 additions, 0 deletions
src/doc/tutorial.md
with
42 additions
and
0 deletions
src/doc/tutorial.md
0 → 100644
+
42
−
0
View file @
7ea0c1c1
Tutorial
========
Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
```
scala
def
size
[
T
](
list
:
List
[
T
])
:
BigInt
=
list
match
{
case
Cons
(
x
,
xs
)
=>
1
+
size
(
xs
)
case
Nil
()
=>
0
}
```
Note that verifying this property requires the use of induction, something Inox does not deal with explicitly.
However, Inox provides all the tools necessary to enable inductive reasonning, as we will see shortly.
Let us start by setting up some useful imports:
```
scala
import
inox._
import
inox.trees._
import
inox.trees.dsl._
```
## ADT Definitions
The dsl we just imported provides us with the following helper methods to define ADTs (see
the
[
Definitions
](
/src/doc/API.md#definitions
)
section in the API documentation for more details):
1.
For ADT sort definitions
```
scala
def
mkSort
(
id
:
Identifier
)
(
tpNames
:
String*
)
(
cons
:
Seq
[
Identifier
])
:
ADTSort
```
2.
For ADT constructor definitions
```
scala
def
mkConstructor
(
id
:
Identifier
)
(
tpNames
:
String*
)
(
sort
:
Option
[
Identifier
])
(
fieldBuilder
:
Seq
[
TypeParameter
]
=>
Seq
[
ValDef
])
:
ADTConstructor
```
We therefore start by
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment