File: foo_after.v

package info (click to toggle)
coq-doc 8.16.1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: bookworm
  • size: 42,788 kB
  • sloc: ml: 219,673; sh: 4,035; python: 3,372; ansic: 2,529; makefile: 728; lisp: 279; javascript: 87; xml: 24; sed: 2
file content (20 lines) | stat: -rw-r--r-- 290 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
 
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5.
  vm_compute; reflexivity.
Qed.