package fstar

You can search for identifiers within the package.

in-package search v0.2.0

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type (!'c, 'm, 'n) matrix_generator =
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under ->
  'c

type (!'c, 'm, 'n) matrix = 'c FStar_Seq_Base.seq

val get_ij : 
  Prims.pos ->
  Prims.pos ->
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under

val get_i : 
  Prims.pos ->
  Prims.pos ->
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under

val get_j : 
  Prims.pos ->
  Prims.pos ->
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under

val transpose_ji : 
  Prims.pos ->
  Prims.pos ->
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under

val seq_of_matrix : 
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

val ijth : 
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq ->
  Prims.int ->
  Prims.int ->
  'c

val matrix_of_seq : 
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

type (!'c, 'm, 'n, 'gen) matrix_of = ('c, Prims.unit, Prims.unit) matrix

val foldm : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c

val init : 
  Prims.pos ->
  Prims.pos ->
  (Prims.int -> Prims.int -> 'c) ->
  'c FStar_Seq_Base.seq

val matrix_seq : 
  Prims.pos ->
  Prims.pos ->
  (Prims.int -> Prims.int -> 'c) ->
  'c FStar_Seq_Base.seq

val transposed_matrix_gen : 
  Prims.pos ->
  Prims.pos ->
  (Prims.int -> Prims.int -> 'c) ->
  Prims.int ->
  Prims.int ->
  'c

type ('c, 'm, 'n, 'eq, 'ma, 'mb) matrix_eq_fun =
  ('c, Prims.unit, Prims.unit, Prims.unit) FStar_Seq_Equiv.eq_of_seq

val matrix_equiv : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq FStar_Algebra_CommMonoid_Equiv.equiv

val matrix_add_generator : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  Prims.int ->
  Prims.int ->
  'c

val matrix_add : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

val matrix_add_zero : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq

val matrix_add_comm_monoid : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  Prims.pos ->
  Prims.pos ->
  ('c FStar_Seq_Base.seq, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm

val col : 
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq ->
  Prims.int ->
  'c FStar_Seq_Base.seq

val row : 
  Prims.pos ->
  Prims.pos ->
  'c FStar_Seq_Base.seq ->
  Prims.int ->
  'c FStar_Seq_Base.seq

val seq_op_const : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c ->
  'c FStar_Seq_Base.seq

val const_op_seq : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

val seq_of_products : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

val dot : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  'c

val matrix_mul_gen : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  Prims.pos ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  Prims.int ->
  Prims.int ->
  'c

val matrix_mul : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  Prims.pos ->
  Prims.pos ->
  Prims.pos ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq ->
  'c FStar_Seq_Base.seq

type ('c, 'eq, 'mul, 'add) is_left_distributive = Prims.unit

type ('c, 'eq, 'mul, 'add) is_right_distributive = Prims.unit

type ('c, 'eq, 'mul, 'add) is_fully_distributive = Prims.unit

type ('c, 'eq, 'z, 'op) is_absorber = Prims.unit

val matrix_mul_unit : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  Prims.pos ->
  'c FStar_Seq_Base.seq