Skip to content

Instantly share code, notes, and snippets.

@spockz
Created September 29, 2010 18:31
Show Gist options
  • Save spockz/603266 to your computer and use it in GitHub Desktop.
Save spockz/603266 to your computer and use it in GitHub Desktop.
data _≤2_ : ℕ → ℕ → Set where
n≤2n : {m : ℕ} → m ≤2 m
n≤2s : {m n : ℕ} → m ≤2 n → m ≤2 suc (n)
from-to : {n m : ℕ} {x : n ≤2 m} -> from (to x) ≡ x
from-to {.m} {m} {n≤2n} = {!refl!}
from-to {n} {suc m} {n≤2s y} = cong ({!n≤2s!}) (from-to {n} {m} {y})
>>
?0 : from (to n≤2n) ≡ n≤2n
?1 : n ≤2 m → n ≤2 suc m
@spockz
Copy link
Author

spockz commented Sep 29, 2010

data ≤2 : ℕ → ℕ → Set where
n≤2n : {m : ℕ} → m ≤2 m
n≤2s : {m n : ℕ} → m ≤2 n → m ≤2 suc (n)

from-to : {n m : ℕ} {x : n ≤2 m} -> from (to x) ≡ x
from-to {.m} {m} {n≤2n} = {!refl!}
from-to {n} {suc m} {n≤2s y} = cong ({!n≤2s!}) (from-to {n} {m} {y})

?0 : from (to n≤2n) ≡ n≤2n
?1 : n ≤2 m → n ≤2 suc m

@kosmikus
Copy link

module ConstraintExample where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

-- An explicit version of refl:

reflx : (n : ℕ) → n ≡ n
reflx n = refl

-- An example of a situation where filling in an expression
-- of the correct type is not sufficient:

example : 2 ≡ 2
example = reflx {!3!}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment