Sha256: 8fdbac821df7786399ff6676a7893d4d27a32f188c17e96fee96482704c3b12e
Contents?: true
Size: 196 Bytes
Versions: 8
Compression:
Stored size: 196 Bytes
Contents
Require Import Coq.Lists.List.
Section with_T.
Context {T : Type}.
Fixpoint length (ls : list T) : nat :=
match ls with
| nil => 0
| _ :: ls => S (length ls)
end.
End with_T.
Version data entries
8 entries across 8 versions & 1 rubygems