aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/mult2.v
blob: 81dede72270944cace5ba104427daf0d72cdb0eb (plain)
1
2
3
4
5
Require Import Arith.
Require mult1.
Definition bar:bool := if le_lt_dec foo 0 then true else false.