You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In this (definitely contrived) example, the foo declaration fails, as evidenced by the fact that it is not in the environment, but no error is reported:
variable (A : Nat) (B : by skip)
deffoo := A = B -- no error is reported#print foo -- unknown constant 'foo'
Using def foo : Prop instead causes the declaration to succeed and report that it uses sorry.
The text was updated successfully, but these errors were encountered:
In this (definitely contrived) example, the
foo
declaration fails, as evidenced by the fact that it is not in the environment, but no error is reported:Using
def foo : Prop
instead causes the declaration to succeed and report that it usessorry
.The text was updated successfully, but these errors were encountered: