Zulip Chat Archive

Stream: new members

Topic: writing and applying axioms


SparkleOyster (Mar 26 2019 at 22:52):

WX20190326-1850562x.png 1553640646699.jpg

As I'm trying to apply the highlighted hypothesis to this axiom I have written, I noticed that the axiom would only take arguments like individual p or q, instead of the whole Prop \not a = b. Is there a way for me to word it so that I can direct apply my hypothesis as in "exact I1 hb1"?

Chris Hughes (Mar 26 2019 at 22:57):

I guess you have variables (p q : point) somewhere? Change the brackets to {} , and it will expect ¬p=q as the first argument.

SparkleOyster (Mar 26 2019 at 23:00):

I guess you have variables (p q : point) somewhere? Change the brackets to {} , and it will expect ¬p=q as the first argument.

Worked! Thank you!


Last updated: Dec 20 2023 at 11:08 UTC