Question about ulib files and naming conventions

[chandradeepdey]

Hi! I wanted to add the following to ulib. Could someone please tell me what files I need to change in the PR and any naming conventions that I need to follow? Also, what about List.Pure and just List?

let rec list_all_mem_implies_subset_lemma (#a: eqtype) (la lb: list a)
    : Lemma (requires (forall x. List.Tot.mem x la ==> List.Tot.mem x lb))
      (ensures (List.Tot.subset la lb)) =
  match la with
  | [] -> ()
  | hd :: tl -> list_all_mem_implies_subset_lemma tl lb

let list_subset_self_lemma (#a: eqtype) (l: list a) : Lemma (List.Tot.subset l l) =
  list_all_mem_implies_subset_lemma l l

[nikswamy]

I would put this in FStar.List.Tot.Properties.

For naming and other conventions, see https://github.com/FStarLang/FStar/wiki/Style-guide

I would be inclined to remove FStar.List.Pure and merge it into FStar.List.Tot, but that's a separate, larger issue.

[chandradeepdey]

Thank you!