seq.Occ: minor change in the definition of occ

(name the lambda that is passed to numof)
parent a1cb7615
......@@ -415,8 +415,9 @@ module Occ
use int.NumOf as N
use import Seq
function occ (x: 'a) (s: seq 'a) (l u: int) : int =
N.numof (fun i -> s[i] = x) l u
function iseq (x: 'a) (s: seq 'a) : int->bool = fun i -> s[i] = x
function occ (x: 'a) (s: seq 'a) (l u: int) : int = N.numof (iseq x s) l u
(* TODO: lemmas for cons, snoc, etc. *)
......
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