Declaration for the special proposition F
Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Assignment 2
Hello Frederik,
I couldn’t make the declaration for False.
Should I put it under the judgements after ded : prop ⟶ type , like fded : prop ⟶ type ?
Best,
Pelin
Hello Pelin,
we discussed this already before the lecture today, but just for the record (if anyone else is interested too):
You can put it after (or before) the declaration of ded. However, ‘false’ has a different type. It’s a proposition.
Best,
Frederik