Tally.Core

Core

A tally is a list of counts. This module defines the type and the two functions the rest of the project reasons about: total and append.

A list of counts.

Inductive tally : Type :=

  | empty : tally
  | cons : nat -> tally -> tally.

References

Uses

Used by

8 more

Declare Scope tally_scope.

Delimit Scope tally_scope with tally.

Infix "::" := cons (at level 60, right associativity) : tally_scope.

References

Uses

Used by

Open Scope tally_scope.

The sum of every count in a tally.

Arguments

the tally summed.

Fixpoint total (t : tally) : nat :=

  match t with
  | empty => 0
  | n :: rest => n + total rest
  end.

Arguments

the tally summed.

References

Uses

Used by

The counts of a, followed by the counts of b.

Arguments

the counts that come first.

the counts that come last.

Fixpoint append (a b : tally) : tally :=

  match a with
  | empty => b
  | n :: rest => n :: append rest b
  end.

Arguments

the counts that come first.

the counts that come last.

References

Uses

Used by

How many counts a tally holds.

Arguments

the tally measured.

Fixpoint size (t : tally) : nat :=

  match t with
  | empty => 0
  | _ :: rest => S (size rest)
  end.

Arguments

the tally measured.

References

Uses

Used by