mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
7095d6c1ed
If they are implicits or class arguments, it's fine for 'auto' to see them since they're only used internally, but interactive proof search will give odd results if it uses them. So, we make a list of names which proof search in interactive mode is allowed to use.
16 lines
374 B
Idris
16 lines
374 B
Idris
import Data.Vect
|
|
|
|
app : Vect n a -> Vect m a -> Vect (n + m) a
|
|
app [] ys = ?app_rhs_1
|
|
app (x :: xs) ys = ?app_rhs_2
|
|
|
|
vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
|
vzipWith f [] [] = ?vzipWith_rhs_3
|
|
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1
|
|
|
|
word_length : Vect n String -> Vect n Nat
|
|
word_length [] = []
|
|
word_length (x :: xs) = ?word_length_rhs_2
|
|
|
|
|