Идрис: восстановить равенство после сопоставления с образцом

Question

Я деконструирую список на голову и хвост, но позже мне нужно доказательство того, что мне возвращают исходный список при объединении:

test: Bool -> String
test b = let lst = the (List Nat) ?getListFromOtherFunction in
        case lst of
          Nil => ""
          x :: xs =>
            let eq = the ((x::xs) = lst) ?howToDoIt in ""

Я использую Idris 1.3.1.

Answer 1

Вы можете сделать это с зависимым сопоставлением с образцом:

test: List Nat -> String
test lst with (lst) proof prf
  | Nil = ""
  | (x :: xs) = ?something

Здесь prf сохранит ваше равенство.

Однако я думаю, что лучше просто сопоставить на lst вLHS, тогда ваши доказательства будут автоматически упрощаться при необходимости.