val list_len : _: Prims.list _ -> Prims.nat
let list_len = length
module Spec.List

open FStar.Calc
open FStar.List.Tot
open Spec.Ubool
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Spec.List.fst
_: Prims.list _ -> Prims.nat
FStar.List.Tot.Base.length Prims.list Prims.nat
let list_len =
  
length