U tweetove putem weba ili aplikacija drugih proizvođača možete dodati podatke o lokaciji, kao što su grad ili točna lokacija. Povijest lokacija tweetova uvijek možete izbrisati. Saznajte više
The "classical five" exercise (Coq'Art, ex 5.7, p. 123) is even more fun in Agda than it is in Coq.
It fits in a (new) tweet. Prove these equivalent: em = ∀ {A : Set} → A ⊎ ¬ A dne = ∀ {A : Set} → ¬ ¬ A → A peirce = ∀ {A B : Set} → ((A → B) → A) → A iad = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B dem = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
The answer doesn't fit in a tweet. But it's five proofs, three of which are two lines long, two of which are four lines long. Really lovely.
Even better: with a couple of imports of work already done in the course, each of the five proofs can be reduced to two lines.
Which means the answer still won't fit in a new tweet. But it will fit into two!
Another benefit is now it's clear this is a reasonable exercise in Proust. It wasn't clear looking at my Coq solutions. So into the LACI flânerie it will go.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.
