aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/mult1.v
blob: 7b6817827688d6f63778b40244dfff97a6142fe5 (plain)
1
2
3
4
5
6
7
8

Require Import Arith.

Definition foo:nat := 1%nat.