Commit f0829ec8 authored by Léo Andrès's avatar Léo Andrès
Browse files

Merge branch 'articles' into 'master'

Removing bad 'pre'

See merge request OCamlPro/www!29
parents 5b4b75fe 3cb724a6
......@@ -36,7 +36,8 @@ As said above, Alt-Ergo makes a clear distinction between Boolean terms and Prop
Last Autumn, we also started working on the integration of algebraic datatypes reasoning in Alt-Ergo. In this first iteration, we extended Alt-Ergo’s native language to be able to declare (mutually recursive) algebraic datatypes, to write expressions with patterns matching, to handle selectors, … We then extended the typechecker accordingly and implemented a (not that) basic theory reasoner. Of course, we also handle SMT2’s algebraic datatypes. Here is an example in Alt-Ergo’s native syntax:
<pre>type ('a, 'b) t = A of {a_1 : 'a} | B of {b_11 : 'a ; b12 : 'b} | C | D | E
```OCaml
type ('a, 'b) t = A of {a_1 : 'a} | B of {b_11 : 'a ; b12 : 'b} | C | D | E
logic e : (int, real) t
logic n : int
......@@ -48,13 +49,13 @@ axiom ax_e:
goal g:
match e with
| A(u) -&gt; u &gt;= 8
| B (u,v) -&gt; u &gt;= 80 and v = 0.
| E -&gt; true
| _ -&gt; false
| A(u) -> u >= 8
| B (u,v) -> u >= 80 and v = 0.
| E -> true
| _ -> false
end
and 3 &lt;= 2+2
</pre>
and 3 <= 2+2
```
## What is planned in 2019 and beyond: the Alt-Ergo’s Users’ Club is born!
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment