Sign in
apache
/
incubator-retired-amaterasu-site
/
ea82bfd9edd5e1015d7640f16e2222ec6d8d34f3
/
.
/
vendor
/
bundle
/
ruby
/
2.4.0
/
gems
/
rouge-1.11.1
/
lib
/
rouge
/
demos
/
coq
blob: c484498899f5422f1d08355eed49036ae42b3e14 [
file
] [
log
] [
blame
]
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
.