Commit d19e084a authored by Nicola Botta's avatar Nicola Botta
Browse files

Added verified setInTo function modifier.

parent adabb546
> module Fun.Operations
> import Basic.Properties
> %default total
> %access public export
......@@ -22,3 +24,24 @@
> modifyFun f a b a' = if a' == a then b else f a'
> |||
> setInTo : {A : Type} -> {B : A -> Type} -> DecEq A =>
> (f : (a : A) -> B a) -> (a : A) -> B a -> ((a : A) -> B a)
> setInTo f a b a' with (decEq a a')
> | (Yes prf) = replace prf b
> | (No contra) = f a'
> setInToSpec1 : {A : Type} -> {B : A -> Type} -> DecEq A =>
> (f : (a : A) -> B a) -> (a : A) -> (b : B a) ->
> setInTo f a b a = b
> setInToSpec1 f a b with (decEq a a)
> | (Yes prf) = replaceLemma prf b
> | (No contra) = void (contra Refl)
> setInToSpec2 : {A : Type} -> {B : A -> Type} -> DecEq A =>
> (f : (a : A) -> B a) -> (a : A) -> (b : B a) ->
> (a' : A) -> Not (a = a') -> setInTo f a b a' = f a'
> setInToSpec2 f a b a' contra' with (decEq a a')
> | (Yes prf) = void (contra' prf)
> | (No contra) = Refl
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment