val equal: #ty: Type -> seq ty -> seq ty -> Type0
let equal (#ty: Type) (s0: seq ty) (s1: seq ty) : Type0 =
  length s0 == length s1 /\
    (forall j.{:pattern index s0 j \/ index s1 j}
      0 <= j && j < length s0 ==> index s0 j == index s1 j)
val equal: #ty: Type -> seq ty -> seq ty -> Type0
let equal (#ty: Type) (s0 s1: seq ty) : Type0 =
length s0 == length s1 /\
(forall j. {:pattern index s0 j\/index s1 j} 0 <= j && j < length s0 ==> index s0 j == index s1 j)
FStar.Sequence.Base.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked
FStar.Sequence.Base.fst
FStar.Sequence.Base.seq Prims.l_and Prims.eq2 Prims.nat FStar.Sequence.Base.length Prims.l_Forall Prims.int Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan Prims.l_imp Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.Sequence.Base.index
(*
   Copyright 2008-2021 Jay Lorch, Rustan Leino, Alex Summers, Dan
   Rosen, Nikhil Swamy, Microsoft Research, and contributors to
   the Dafny Project

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Includes material from the Dafny project
   (https://github.com/dafny-lang/dafny) which carries this license
   information:

     Created 9 February 2008 by Rustan Leino.
     Converted to Boogie 2 on 28 June 2008.
     Edited sequence axioms 20 October 2009 by Alex Summers.
     Modified 2014 by Dan Rosen.
     Copyright (c) 2008-2014, Microsoft.
     Copyright by the contributors to the Dafny Project
     SPDX-License-Identifier: MIT
*)

(**
This module declares a type and functions used for modeling sequences
as they're modeled in Dafny. It also states and proves some properties
about sequences, and provides a lemma `all_seq_facts_lemma` one
can call to bring them into context.  The properties are modeled after
those in the Dafny sequence axioms, with patterns for quantifiers
chosen as in those axioms.

@summary Type, functions, and properties of sequences
*)
module FStar.Sequence.Base

module FLT = FStar.List.Tot

/// Internally, we represent a sequence as a list.

type seq (ty: Type) = list ty

/// We represent the Dafny function `Seq#Length` with `length`:
///
/// function Seq#Length<T>(Seq T): int;

let length = FLT.length

/// We represent the Dafny function `Seq#Empty` with `empty`:
/// 
/// function Seq#Empty<T>(): Seq T;

let empty (#ty: Type) : seq ty = []

/// We represent the Dafny function `Seq#Singleton` with `singleton`:
///
/// function Seq#Singleton<T>(T): Seq T;

let singleton (#ty: Type) (v: ty) : seq ty =
  [v]

/// We represent the Dafny function `Seq#Index` with `index`:
///
/// function Seq#Index<T>(Seq T, int): T;

let index (#ty: Type) (s: seq ty) (i: nat{i < length s}) : ty =
  FLT.index s i

/// We represent the Dafny function `Seq#Build` with `build`:
/// 
/// function Seq#Build<T>(s: Seq T, val: T): Seq T;

let build (#ty: Type) (s: seq ty) (v: ty) : seq ty =
  FLT.append s [v]

/// We represent the Dafny function `Seq#Append` with `append`:
///
/// function Seq#Append<T>(Seq T, Seq T): Seq T;

let append = FLT.append

/// We represent the Dafny function `Seq#Update` with `update`:
///
/// function Seq#Update<T>(Seq T, int, T): Seq T;

let update (#ty: Type) (s: seq ty) (i: nat{i < length s}) (v: ty) : seq ty =
  let s1, _, s2 = FLT.split3 s i in
  append s1 (append [v] s2)

/// We represent the Dafny function `Seq#Contains` with `contains`:
///
/// function Seq#Contains<T>(Seq T, T): bool;

let contains (#ty: Type) (s: seq ty) (v: ty) : Type0 =
  FLT.memP v s

/// We represent the Dafny function `Seq#Take` with `take`:
///
/// function Seq#Take<T>(s: Seq T, howMany: int): Seq T;

let take (#ty: Type) (s: seq ty) (howMany: nat{howMany <= length s}) : seq ty =
  let result, _ = FLT.splitAt howMany s in
  result

/// We represent the Dafny function `Seq#Drop` with `drop`:
///
/// function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;

let drop (#ty: Type) (s: seq ty) (howMany: nat{howMany <= length s}) : seq ty =
  let _, result = FLT.splitAt howMany s in
  result

/// We represent the Dafny function `Seq#Equal` with `equal`.
///
/// function Seq#Equal<T>(Seq T, Seq T): bool;
val equal: #ty: Type -> seq ty -> seq ty -> Type0
s0: FStar.Sequence.Base.seq ty -> s1: FStar.Sequence.Base.seq ty -> Type0