[Agda] type of []

[Sergei Meshveliani]

On Tue, 2018-04-17 at 12:52 +0000, Thorsten Altenkirch wrote:
> Not sure what is the "regular" way but could you not just supply the implicit argument to [] (or to take)?
> 
> take-n-[] :  ∀ {α} {A : Set α} {n} → take n ([] {A}) ≡ []
> 
> or
> 
> take-n-[] :  ∀ {α} {A : Set α} {n} → take {A} n [] ≡ []
> 


Thank you. 
This is exactly what is needed.
I knew that I was missing some simple point, but just did not recall
that `take' or [] can be given implicit argument!

------
Sergei



> On 17/04/2018, 13:45, "Agda on behalf of Sergei Meshveliani" <agda-bounces at lists.chalmers.se on behalf of mechvel at botik.ru> wrote:
> 
>     People,
>     
>     In the proof
>     
>       take-n-[] :  {n : ℕ} → take n [] ≡ []
>       take-n-[] {0}     =  refl
>       take-n-[] {suc _} =  refl
>     
>     Agda cannot derive the type of []. 
>     I can fix the signature in two ways.
> [..]