vendor/bundle/ruby/3.4.0/gems/rouge-4.7.0/lib/rouge/demos/coq


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

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".
Definition escape_string := "0123".
Definition zero_string := "0".