Multiple (decreases ...) clauses

[gebner]

Right now, the harness fails on some mutually recursive lemmas because it puts one decreases on the val for the lemma that we check and on the let rec for the other lemmas in the block.

This also happens with single let recs:

val  elim_of_list'': #a: Type -> i: nat -> s: seq a -> l: list a
  -> Lemma
      (requires
        (List.Tot.length l + i = length s /\ i <= length s /\ slice s i (length s) == seq_of_list l)
      ) (ensures (explode_and i s l)) (decreases (List.Tot.length l))
let rec elim_of_list'': #a:Type ->
  i:nat ->
  s:seq a ->
  l:list a ->
  Lemma
    (requires (
      List.Tot.length l + i = length s /\
      i <= length s /\
      slice s i (length s) == seq_of_list l))
    (ensures (
      explode_and i s l))
    (decreases (
      List.Tot.length l))
= fun #_ i s l ->
  match l with
  | [] -> ()
  | hd :: tl ->
      lemma_seq_of_list_induction l;
      elim_of_list'' (i + 1) s tl