Имена зависимых переменных в Idris - PullRequest
Новая
       47

Имена зависимых переменных в Idris

0 голосов
/ 16 февраля 2019

Можно ли указать имя зависимой переменной в Idris?Я хотел бы динамически генерировать функцию, которая принимает натуральные числа, которые названы точно так же, как входной вектор символов?Возможно ли это в Idris?

У меня есть рабочая функция fn, которая создает зависимую функцию, но с неверно названными переменными. 

fn : Vect n Char -> Type -> Vect m Nat -> Type
fn [] a ys = Tensor ys a
fn (x :: xs) a ys = (i : Nat) -> fn xs a (i::ys)


data Tensor : Vect rank Nat -> Type -> Type where
    ....

Ожидаемый результат: 

λΠ> fn ['i','j','k'] Double []
(i : Nat) -> (j : Nat) -> (k : Nat) -> Tensor [i, j, k] Double : Type

Фактический результат: 

λΠ> fn ['i','j','k'] Double []
(i : Nat) -> (i1 : Nat) -> (i2 : Nat) -> Tensor [i2, i1, i] Double : Type
...