lean2/tests/lean/run/let2.lean
2014-08-28 16:27:52 -07:00

23 lines
464 B
Text

import logic
definition b :=
let a := true ∧ true,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a,
a := a ∧ a in
a
check b