-
Notifications
You must be signed in to change notification settings - Fork 232
Documenting the library
Santiago Zanella-Beguelin edited this page Oct 10, 2019
·
19 revisions
| Assigned to | File name | Rename to? | Move to? | Notes |
|---|---|---|---|---|
| FStar.Algebra.CommMonoid.fst | math | |||
| FStar.Algebra.Monoid.fst | math | |||
| nik | FStar.All.fst | FStar.Effect.ML | effects | |
| FStar.Array.fst | legacy | Superceded by LowStar.Buffer? | ||
| FStar.Array.fsti | legacy | idem | ||
| FStar.Axiomatic.Array.fst | legacy | idem | ||
| nik | FStar.BaseTypes.fsti | core | ||
| FStar.BigOps.fst | core | |||
| FStar.BigOps.fsti | core | |||
| FStar.BitVector.fst | core | |||
| FStar.Buffer.fst | legacy | |||
| FStar.Buffer.Quantifiers.fst | legacy | |||
| FStar.BufferNG.fst | legacy | |||
| nik | FStar.BV.fst | core | ||
| nik | FStar.BV.fsti | core | ||
| FStar.Bytes.fsti | FStar.Native.Bytes? | native | ||
| FStar.Calc.fst | core | |||
| nik | FStar.Char.fsti | FStar.Native.Char | native | |
| denis/jay | FStar.Classical.fst | FStar.Squash.Properties? | core | |
| denis/jay | FStar.Classical.fsti | FStar.Squash.Properties? | core | |
| nik | FStar.ConstantTime.Integers.fst | experimental | ||
| nik | FStar.ConstantTime.Integers.fsti | experimental | ||
| FStar.Constructive.fst | legacy | these are now in prims | ||
| FStar.Crypto.fst | legacy | |||
| nik | FStar.Date.fsti | FStar.Native.Date | native | |
| nik | FStar.DependentMap.fst | container | ||
| nik | FStar.Dyn.fsti | FStar.Native.Dyn | native | |
| FStar.Endianness.fst | core | |||
| FStar.Endianness.fsti | core | |||
| nik | FStar.ErasedLogic.fst | legacy | ||
| FStar.Error.fst | legacy? | superceded by Prims.either | ||
| FStar.Exn.fst | FStar.Native.Exn | native | ||
| FStar.Fin.fst | FStar.Finiteness? | math; partially experimental (finish?) | ||
| FStar.Float.fsti | FStar.Native.Float | native | ||
| nik | FStar.FunctionalExtensionality.fst | core | ||
| nik | FStar.FunctionalExtensionality.fsti | core | ||
| nik | FStar.Ghost.fsti | FStar.Erased? | core | |
| aseem | FStar.GSet.fst | FStar.GhostSet? | container | |
| aseem | FStar.GSet.fsti | FStar.GhostSet? | container | |
| aseem | FStar.Heap.fst | memory-model | ||
| aseem | FStar.HyperStack.All.fst | FStar.Effect.HyperStack.ML? | effect | |
| aseem | FStar.HyperStack.fst | memory-model | ||
| FStar.HyperStack.IO.fst | legacy | merge with FStar.Effect.HyperStack.ML? | ||
| aseem | FStar.HyperStack.ST.fst | FStar.Effect.HyperStack.ST | effect | |
| aseem | FStar.HyperStack.ST.fsti | FStar.Effect.HyperStack.ST | effect | |
| nik | FStar.IFC.fst | |||
| FStar.IndefiniteDescription.fst | core | |||
| FStar.Int.Cast.fst | numeric | |||
| FStar.Int.Cast.Full.fst | numeric (merge with FStar.Int.Cast)? | |||
| FStar.Int.fst | numeric | |||
| FStar.Int128.fst | numeric | |||
| FStar.Int16.fst | numeric | |||
| FStar.Int31.fst | numeric | |||
| FStar.Int32.fst | numeric | |||
| FStar.Int63.fst | numeric | |||
| FStar.Int64.fst | numeric | |||
| FStar.Int8.fst | numeric | |||
| FStar.Integers.fst | numeric | |||
| FStar.IO.fst | core | |||
| FStar.List.fst | container | |||
| FStar.List.Pure.Base.fst | container | |||
| FStar.List.Pure.fst | container | |||
| FStar.List.Pure.Properties.fst | container | |||
| FStar.List.Tot.Base.fst | container | |||
| FStar.List.Tot.fst | container | |||
| FStar.List.Tot.Properties.fst | container | |||
| aseem | FStar.Map.fst | container | ||
| aseem | FStar.Map.fsti | container | ||
| FStar.MarkovsPrinciple.fst | math | |||
| aymeric | FStar.Math.Lemmas.fst | math | ||
| FStar.Math.Lib.fst | math | |||
| FStar.Matrix2.fsti | legacy | container | ||
| FStar.Modifies.fst | memory-model | |||
| FStar.Modifies.fsti | memory-model | |||
| FStar.ModifiesGen.fst | memory-model | |||
| FStar.ModifiesGen.fsti | memory-model | |||
| FStar.Monotonic.DependentMap.fst | container | |||
| FStar.Monotonic.DependentMap.fsti | container | |||
| aseem | FStar.Monotonic.Heap.fst | memory-model | ||
| aseem | FStar.Monotonic.Heap.fsti | memory-model | ||
| aseem | FStar.Monotonic.HyperHeap.fst | memory-model | ||
| aseem | FStar.Monotonic.HyperHeap.fsti | memory-model | ||
| aseem | FStar.Monotonic.HyperStack.fst | memory-model | ||
| aseem | FStar.Monotonic.HyperStack.fsti | memory-model | ||
| aseem | FStar.Monotonic.Map.fst | container | ||
| aseem | FStar.Monotonic.Seq.fst | container | ||
| aseem | FStar.Monotonic.Witnessed.fst | memory-model | ||
| aseem | FStar.Monotonic.Witnessed.fsti | memory-model | ||
| aseem | FStar.MRef.fst | memory-model | ||
| FStar.Mul.fst | core | |||
| FStar.Option.fst | core | |||
| aseem | FStar.Order.fst | math | ||
| aseem | FStar.OrdMap.fst | container | ||
| aseem | FStar.OrdMapProps.fst | container | ||
| aseem | FStar.OrdSet.fst | container | ||
| aseem | FStar.OrdSetProps.fst | container | ||
| FStar.Pervasives.fst | core | |||
| FStar.Pervasives.Native.fst | core | |||
| FStar.Pointer.Base.fst | legacy | memory-model | ||
| FStar.Pointer.Base.fsti | legacy | memory-model | ||
| FStar.Pointer.Derived1.fst | legacy | memory-model | ||
| FStar.Pointer.Derived1.fsti | legacy | memory-model | ||
| FStar.Pointer.Derived2.fst | legacy | memory-model | ||
| FStar.Pointer.Derived2.fsti | legacy | memory-model | ||
| FStar.Pointer.Derived3.fst | legacy | memory-model | ||
| FStar.Pointer.Derived3.fsti | legacy | memory-model | ||
| FStar.Pointer.fst | legacy | memory-model | ||
| FStar.PredicateExtensionality.fst | core | |||
| aseem | FStar.Preorder.fst | math | ||
| FStar.Printf.fst | core | |||
| FStar.PropositionalExtensionality.fst | core | |||
| FStar.Range.fsti | native | |||
| FStar.Reader.fst | effect | |||
| FStar.Real.fsti | numeric | |||
| aseem | FStar.Ref.fst | memory-model | ||
| FStar.Reflection.Arith.fst | reflection | |||
| FStar.Reflection.Basic.fst | reflection | |||
| FStar.Reflection.Const.fst | reflection | |||
| FStar.Reflection.Data.fst | reflection | |||
| FStar.Reflection.Derived.fst | reflection | |||
| FStar.Reflection.Derived.Lemmas.fst | reflection | |||
| FStar.Reflection.Formula.fst | reflection | |||
| FStar.Reflection.fst | reflection | |||
| FStar.Reflection.Types.fsti | reflection | |||
| santiago | FStar.ReflexiveTransitiveClosure.fst | math | ||
| santiago | FStar.ReflexiveTransitiveClosure.fsti | math | ||
| FStar.Relational.Comp.fst | legacy | |||
| FStar.Relational.Relational.fst | legacy | |||
| FStar.Relational.State.fst | legacy | |||
| FStar.Seq.Base.fst | container | |||
| FStar.Seq.fst | container | |||
| FStar.Seq.Properties.fst | container | |||
| FStar.Seq.Sorted.fst | container | |||
| aseem | FStar.Set.fst | container | ||
| aseem | FStar.Set.fsti | container | ||
| aseem | FStar.Squash.fst | core | ||
| aseem | FStar.Squash.fsti | core | ||
| aseem | FStar.SquashProperties.fst | core | ||
| aseem | FStar.ST.fst | effect | ||
| FStar.String.fsti | native | |||
| FStar.StrongExcludedMiddle.fst | core | |||
| FStar.Tactics.Arith.fst | tactics | |||
| FStar.Tactics.Builtins.fst | tactics | |||
| FStar.Tactics.BV.fst | tactics | |||
| FStar.Tactics.Canon.fst | tactics | |||
| FStar.Tactics.CanonCommMonoid.fst | tactics | |||
| FStar.Tactics.CanonCommMonoidSimple.fst | tactics | |||
| santiago | FStar.Tactics.CanonCommSemiring.fst | tactics | ||
| FStar.Tactics.CanonCommSwaps.fst | tactics | |||
| FStar.Tactics.CanonMonoid.fst | tactics | |||
| FStar.Tactics.Derived.fst | tactics | |||
| FStar.Tactics.Effect.fst | tactics | |||
| FStar.Tactics.fst | tactics | |||
| FStar.Tactics.Logic.fst | tactics | |||
| FStar.Tactics.PatternMatching.fst | tactics | |||
| FStar.Tactics.Result.fst | tactics | |||
| FStar.Tactics.Simplifier.fst | tactics | |||
| FStar.Tactics.Typeclasses.fst | tactics | |||
| FStar.Tactics.Types.fsti | tactics | |||
| FStar.Tactics.Util.fst | tactics | |||
| FStar.TaggedUnion.fst | legacy | |||
| FStar.TaggedUnion.fsti | legacy | |||
| FStar.Tcp.fsti | native | |||
| aseem | FStar.TSet.fst | container | ||
| FStar.TwoLevelHeap.fst | legacy | memory-model | ||
| FStar.Udp.fsti | container | |||
| FStar.UInt.fst | numeric | |||
| FStar.UInt128.fst | numeric | |||
| FStar.UInt128.fsti | numeric | |||
| FStar.UInt16.fst | numeric | |||
| FStar.UInt31.fst | numeric | |||
| FStar.UInt32.fst | numeric | |||
| FStar.UInt63.fst | numeric | |||
| FStar.UInt64.fst | numeric | |||
| FStar.UInt8.fst | numeric | |||
| aseem | FStar.Universe.fst | core | ||
| aseem | FStar.Universe.fsti | core | ||
| FStar.Util.fst | core (defunct?) | |||
| FStar.Vector.Base.fst | container | |||
| FStar.Vector.Base.fsti | container | |||
| FStar.Vector.fst | container | |||
| FStar.Vector.Properties.fst | container | |||
| FStar.WellFounded.fst | math | |||
| LowStar.Buffer.fst | container | |||
| LowStar.BufferCompat.fst | legacy | |||
| LowStar.BufferOps.fst | container | |||
| LowStar.BufferView.Down.fst | container | |||
| LowStar.BufferView.Down.fsti | container | |||
| LowStar.BufferView.fst | container | |||
| LowStar.BufferView.fsti | container | |||
| LowStar.BufferView.Up.fst | container | |||
| LowStar.BufferView.Up.fsti | container | |||
| LowStar.ConstBuffer.fst | container | |||
| LowStar.ConstBuffer.fsti | container | |||
| LowStar.Endianness.fst | core | |||
| LowStar.ImmutableBuffer.fst | container | |||
| LowStar.Literal.fsti | core | |||
| LowStar.Modifies.fst | memory-model | |||
| LowStar.ModifiesPat.fst | memory-model | |||
| LowStar.Monotonic.Buffer.fst | container | |||
| LowStar.Monotonic.Buffer.fsti | container | |||
| LowStar.PrefixFreezableBuffer.fst | container | |||
| LowStar.PrefixFreezableBuffer.fsti | container | |||
| LowStar.Printf.fst | core | |||
| LowStar.Regional.fst | memory-model | |||
| LowStar.Regional.Instances.fst | memory-model | |||
| LowStar.RVector.fst | container | |||
| LowStar.ToFStarBuffer.fst | legacy | |||
| LowStar.UninitializedBuffer.fst | container | |||
| LowStar.Vector.fst | container | |||
| aseem | prims.fst | FStar.Prims? | core |