Tutorial - Propositional Logic

[mtnrbq]

In the tutorial, the following example is used:
... shows how to prove that if p implies q and q implies r, then p implies r

and translates it to:

(define-fun conjecture () Bool
	(=> (and (= p q) (= q r))
		(= p r)))

i.e. using Bi-implication

Would it not be more correct to use Implication as per the text of the proposition ?
i.e.

(define-fun conjecture () Bool
	(=> (and (=> p q) (=> q r))
		(=> p r)))

[NikolajBjorner]

Thanks, fixed.
Note that there is also an option to add a pull request directly to the page following
Edit this page