Better way to write constructors as a function in Agda
I have a list
data List (X : Set) : Set where
<> : List X
_,_ : X -> List X -> List X
definition of equality
data _==_ {l}{X : Set l}(x : X) : X -> Set l where
refl : x == x
and congruence
cong : forall {k l}{X : Set k}{Y : Set l}(f : X -> Y){x y} -> x == y -> f x == f y
cong f refl = refl
I'm trying to prove
propFlatten2 : {X : Set } ( xs0 : List X ) (x : X) (xs1 : List X) (xs2 : List X)
-> ( xs0 ++ x , xs1 ) ++ xs2 == xs0 ++ (x , xs1 ++ xs2 )
propFlatten2 <> x xs1 xs2 = refl
propFlatten2 (x , xs0) x₁ xs1 xs2 = cong (λ l -> x , l) {!!}
Is there a better way to use the constructor directly _,_
, other than via the lambda on the last line?
source to share
Agda does not have a specific syntax for partial operator application. However, you can use the operators in your normal prefixed version:
x + y = _+_ x y
This is handy if you need to partially apply the left argument (s):
_+_ 1 = λ x → 1 + x
If you need to partially apply the arguments on the right, your options are more limited. As mentioned in the comments, you can use one of the handy functions like flip
(found in Function
):
flip f x y = f y x -- Type omitted for brevity.
And then just the flip
arguments _+_
:
flip _+_ 1 = λ x → x + 1
Sometimes you will find operators whose sole purpose is to make your code a little nicer. The best example I can think of is probably Data.Product.,_
. When you write a dependent pair ( Data.Product.Σ
), sometimes the first part of the pair can be filled in automatically. Instead of writing:
_ , x
You can simply write:
, x
It's hard to tell when writing a specialized operator like the one above is really worth it; if your only use case is using it with congruence, I just stick with the lambda as it is very clear about what is going on.
source to share