Assignment 2

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.

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