Question

我撰写的《科克法典》需要修改名单,特别是使用索引i,将功能应用到该要素,并替换该功能。我可以使用.Coq.Lists.List.List. 然后,我可以把这一功能运用到这一要素上,但用<条码>Coq.List.List的图书馆,将内容重新列入原始名单的最佳方式是什么?

我目前有以下法典:

Definition bv (n : nat) := list bool. 
Definition get_bv {n : nat} (i : nat) (v : bv n) := nth i v false.
Notation " v [ i ]" := (get_bv i v) (at level 0).

因此,鉴于我想要应用<代码>f:bool->bool的功能,我可以使用f(v[i],但我并不肯定如何取代。

Answer 1

If you want to apply the same function to every element of a list, you can use map. Instead if you want to only replace one single element of a list, you may need to write your own replace function. For example:

Require Import List.
Import ListNotations.

Fixpoint replace {A : Type} (l : list A)  (i : nat) (v : A) := 
  match l with 
  | [] => []
  | a :: l1 => match i with 
               |    0 => v :: l1 
               | S i1 => a :: replace l1 i1 v 
               end 
  end.

Compute replace [true; false; true] 2 false.

Answer 2

Coq采用功能式方案拟订模式,因此,你不能“取代”一种你用必要的方案拟订语言编写的要素。但是,你可以制定一份新名单,其要素为:i, 即f (v[i], 而不是(old)v[i], 所有其他内容与原始名单相同。

请注意,数学比较<代码>seq.v的图书馆已经提供了准确的<代码>_nth功能。

友情链接