louisswarren · April 16, 2019 00:19
diff --git a/strange.agda b/strange.agda
 data ⊥ : Set where

 hmm : ∀ α → ⊥
 -- Agda infers that
 --   α : ⊥
 -- because that's only way this could be provable?
 hmm α = α
	data ⊥ : Set where

	hmm : ∀ α → ⊥
	-- Agda infers that
	-- α : ⊥
	-- because that's only way this could be provable?
	hmm α = α