Commit f66b8de5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some typing errors in examples.

parent 3f65d6fa
......@@ -80,7 +80,7 @@ predicate eval_fmla (sigma:env) (pi:env) (f:fmla) =
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is fresh *)
function subst_term (e:term) (r:ident) (v:ident) : term =
let rec function subst_term (e:term) (r:ident) (v:ident) : term =
match e with
| Tconst _ -> e
| Tvar _ -> e
......@@ -117,7 +117,7 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
| Fforall y _ f -> id <> y /\ fresh_in_fmla id f
end
function subst (f:fmla) (x:ident) (v:ident) : fmla =
let rec function subst (f:fmla) (x:ident) (v:ident) : fmla =
match f with
| Fterm e -> Fterm (subst_term e x v)
| Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
......
......@@ -37,8 +37,11 @@ end
theory Divisibility
use export int.Int
use import int.ComputerDivision
predicate divides (d:int) (n:int) = exists q:int. n = q * d
let predicate divides (d:int) (n:int)
ensures { result <-> exists q:int. n = q * d }
= if d = 0 then n = 0 else mod n d = 0
lemma divides_refl: forall n:int. divides n n
lemma divides_1_n : forall n:int. divides 1 n
......
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