louisswarren
/ implicit.agda
Last active Mar 21, 2019
— forked from milesrout/meme.agda
View implicit.agda
| open import Agda.Builtin.Bool | |
| data ⊥ : Set where | |
| record ⊤ : Set where | |
| isTrue : Bool → Set | |
| isTrue true = ⊤ | |
| isTrue false = ⊥ | |
| data ℕ : Set where |