: is used for type annotations instead of :: like in Haskell. The double asterisk is syntactic sugar for a "dependent pair" http://docs.idris-lang.org/en/lates

: is used for type annotations instead of :: like in Haskell. The double asterisk is syntactic sugar for a "dependent pair" http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-pairs http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... Basically, it is a pair in which the type of the second element depends on the value of the first element. Here it is being used to pack the result list with a proof that the list satisfies the required properties. The type of the proof must refer to the list, hence the need for dependent types. The stuff within braces {} are implicit arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=braces#implicit-arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... that are not given explicitly, but are inferred from the type of other arguments. Type is commonly referred as the kind * in Haskell, the kind of types that have values. Unlike in vanilla Haskell, the types of data constructors are explicitly stated http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=data#vectors http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... In Haskell the "types" of data constructors are kinds, and you need to enable the XKindSignatures extension to give them explicitly. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=#extension-KindSignatures https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...