如何在列表中应用图案匹配

Question

我正在对l'进行归纳。当第一次进行归纳时，我遇到了两种情况，[]和n::l''，第二次归纳后为n::[],n::n0::t。我想简化一下，在进行了两次归纳后。

f1(match l' with
| [] => n
| _ :: _ => high_v (length l')(change n l')
         end + m) (n :: l').

Answer 1

在目前的问题措辞中，我猜测存在一个类型的 A (可能是 A 是 nat)，并且该功能 change 和 high_v 有型 nat -> list nat -> A 和 nat -> A -> nat 分别是。 如果文中是对当前目标的陈述，那么我猜想 f1 必有型 nat -> list nat -> Prop. 你能确认吗？

以目前问题的措辞，恐怕我们帮不了你。