File: foo_after.v

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; 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.