File: foo_after.v

package info (click to toggle)
coq 8.12.0-3
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 36,468 kB
  • sloc: ml: 210,451; sh: 3,345; python: 3,008; ansic: 2,482; makefile: 793; lisp: 224; 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.