Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/letNeeded Secret

Created May 4, 2014 21:56
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gallais/7468215361cdcfe09c7b to your computer and use it in GitHub Desktop.
Save gallais/7468215361cdcfe09c7b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
letNeeded
module letNeeded where
open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality
lemmaOk : 3 ≡ 3
lemmaOk =
let n = 3
in n ≡ 3 ∋ refl
lemmaFail : 3 ≡ 3
lemmaFail =
(((n : ℕ) → n ≡ 3) ∋ (λ n → refl)) 3
{-
/home/gallais/languages/agda/letNeeded.agda:14,31-35
n != suc 2 of type ℕ
when checking that the expression refl has type n ≡ 3
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment