python.mlw 415 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22

module Python

  use import int.Int
  use import ref.Ref
  use seq.Seq as S

  type list 'a = ref (S.seq 'a)

  function ([]) (l: list 'a) (i: int) : 'a =
    S.([]) !l i

  let ([]) (l: list 'a) (i: int) : 'a
    requires { 0 <= i < S.length !l }
    ensures  { result = l[i] }
  = S.([]) !l i

  val range (l u: int) : list int
    requires { l <= u }
    ensures  { forall i. l <= i < u -> result[i] = i }

end