Skip to content

Instantly share code, notes, and snippets.

@canonic-epicure
Created June 1, 2018 17:23
Embed
What would you like to do?
module Exprm_FunctionImage where
open import Data.Vec
open import Data.List
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x
module FunctionImage where
data FunctionImage1 : {A B : Set} -> (f : A -> B) -> A -> B -> Set where
MkFunctionImage1 : {A B : Set} -> {f : A -> B} -> (a : A) -> FunctionImage1 f a (f a)
data FunctionImage2 : {A B C : Set} -> (f : A -> B -> C) -> A -> B -> C -> Set where
MkFunctionImage2 : {A B C : Set} -> (f : A -> B -> C) -> (a : A) -> (b : B) -> FunctionImage2 f a b (f a b)
example1 : FunctionImage1 Data.Vec.sum (1 ∷ 2 ∷ []) 3
example1 = MkFunctionImage1 (1 ∷ 2 ∷ [])
example2 : FunctionImage1 Data.Vec.reverse (1 ∷ 2 ∷ []) (2 ∷ 1 ∷ [])
example2 = MkFunctionImage1 (1 ∷ 2 ∷ [])
module ListHasExactlyOneElement where
open FunctionImage
data ListHasExactlyOneElement : {A : Set} -> List A -> Set where
ItDoes : {A : Set} -> {list : List A} -> FunctionImage1 (Data.List.length) list 1 -> ListHasExactlyOneElement {A} list
getElementFromProof : {A : Set} -> {xs : List A} -> (prf : ListHasExactlyOneElement {A} xs) -> A
getElementFromProof (ItDoes {A = ty} imagePrf) =
case imagePrf of \ {
(MkFunctionImage1 a) -> {!z!}
}
{-
I'm not sure if there should be a case for the constructor
MkFunctionImage1, because I get stuck when trying to solve the
following unification problems (inferred index ≟ expected index):
{_} ≟ {_}
{_} ≟ {_}
f ≟ length
a ≟ .xs
f a ≟ 1
when checking that the pattern MkFunctionImage1 a has type
FunctionImage1 length .xs 1
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment