[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] The 'suppose' keyword
- To: mizar-forum@mizar.uwb.edu.pl
- Subject: Re: [mizar] The 'suppose' keyword
- From: Boris Schminke <schminkeba@gmail.com>
- Date: Sat, 24 Apr 2010 23:28:06 +0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=gKV6G45anJ7YilhSTKSUYR8AfC6IKmyeQgjNIO6edPi28GQ9vUezpbBMNNHX0s9A8v TBILoV6FGOxKlLvGlwwMJF3yRtoEbaHWMO203Z+SsenIz/WewLSdmUdGP+wsbpm/Fijw +UW0cSqZBP0IAPJtYjhPMyEIwrZgCLS2bxADM=
Dear Piotr,
I've found in the article EUCLID_3 examples of using both 'case' and
'suppose' keywords in 'per cases'. When I tried to change 'suppose' to
'case' and vice versa the proofs was still passing verification.
Therefore, I guess that it's more likely that they are synonymic than
anything else. Although, it's not clear is the existence of these two
keywords a kind of syntactic sugar or there is something more to it.
Thanks for your answer anyway.
Best regards,
Schminke Boris.