2014-10-05 17:50:13 +00:00
|
|
|
import data.prod data.num logic.quantifiers
|
2015-10-13 22:39:03 +00:00
|
|
|
open prod nat
|
2014-09-04 21:21:03 +00:00
|
|
|
|
2015-10-13 22:39:03 +00:00
|
|
|
check (true, false, (10:nat))
|
2014-09-04 21:21:03 +00:00
|
|
|
|
|
|
|
-- definition a f := f
|
|
|
|
|
|
|
|
check fun x, x ∧ x
|