13 lines
238 B
Plaintext
13 lines
238 B
Plaintext
|
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.
|
||
|
|
|
||
|
|
Definition a_string := "hello \" world".
|