stelliferous

Releases (2)

• 0.0.3.0 invalid

  expected a fresh constructor name (duplicate declaration: Text)

  at checkpoint_pickle.bend:14

  8 files do not load

  • checkpoint_pickle.bend
  • tensor_batch_norm.bend
  • tensor_checkpoint.bend
  • tensor_f32.bend
  • tensor_layer.bend
  • tensor_loss.bend
  • tensor_optimizer.bend
  • tensor_training.bend
• 0.0.2.0 indexed

Definitions (2,086)

proofs/kernel_packing_witness.bend

• type CrossingCursor
• def restore_crossing
• type CrossingEvidence
• def stored_crossing
• def store_crossing
• def crossing
• def crossing_loop
• type TileCursor
• def restore_tiles
• type TileEvidence
• def after_row_tile
• def after_crossing
• def tile
• def tile_step
• def tile_loop
• def finish
• def pack

proofs/kernel_read_witness.bend

• type LoopedThe k loop returns every owner it received.
• def after_input
• def after_weights
• def step_at
• def step
• def run

proofs/kernel_tile_witness.bend

• def pairPair composition consumes already established observations.
• def finish
• def with_head
• def pair_head
• def four_head
• def eight_head
• def tail

proofs/kernel_weights_certificate.bend

• def family
• def block
• def traverse
• def finish
• def allocated
• def run
• def equation
• def certificate

proofs/kernel_weights_witness.bend

• def conditionalMissing rows are zero-filled without changing the source owner.
• def eighth
• def seventh
• def sixth
• def fifth
• def fourth
• def third
• def second
• def first
• def read

proofs/loop_projection.bend

• def iterate
• def iteration_refines_modelA single commuting step lifts to every count.
• def preserves_observationA read-only observation is preserved for every number of iterations.
• def iteration_matches_denotation
• type Measured
• def add_work
• def measured_iteration
• def iteration_result_and_workConcrete adapters must establish cost_per_step; it is not a heap-cost claim.
• def indexed_successor
• def add_counted_stride
• def counter_progress
• def run_then_finishesThe final step is applied once, to the state the loop ends in.

proofs/nat_division.bend

• def lt_zero
• def lt_succ_le
• def go_small
• def small
• def bump
• def bumped_quotient
• law bump_go
• law cycle
• def add_divisor
• law quotient_remainder
• def unique

proofs/nat_extrema.bend

• def successor_pick
• def minimum_choice
• def maximum_choice
• def minimum_when_ordered
• def minimum_left
• def minimum_right
• def maximum_left
• def maximum_right
• def pick_upper
• def pick_lower
• def pick_strict_lower
• def maximum_upper
• def minimum_lower
• def minimum_strict_lower
• def minimum_monotone
• def clipped_end
• def below_zero_right
• def below_minimumA lane belongs to a clipped count exactly when it belongs to both bounds.

proofs/nat_interval.bend

• def shifted_inside
• def shifted_span
• type OutsideA query lies strictly before or at/after the end of a half-open interval.
• def outside_head
• def outside_tail

proofs/nat_order.bend

• def not_below
• def cancel_offset_le
• def equal_of_is_eq
• def subtract_zero
• def zero_subtract
• def subtract_shift