File Edit View Navigation Templates Queries Tools Compile Debug Windows Help projectfianl ex_02_sumlist Require Import Coq.Lists. List. Import ListNotations. Section LinkedList. Variable A: Type. Inductive LinkedList = LNil LCons (x: A) (xs LinkedList). End LinkedList. Section Append. Fixpoint append (xs ys: LinkedList) : LinkedList := match xs with LNil => ys | LCons x xs' => LCons x (append xs' ys) end. End Append. From iris.base_logic Require Import invariants. From iris.proofmode Require Import tactics. Section AppendProof. Context inG E (authR (listUR A))). Lemma append_nil_r (xs: LinkedList) Proof. induction xs; simpl; auto. Qed. append xs LNil xs. Lemma append_assoc (xs ys zs LinkedList) : append (append xs ys) zs = append xs (append ys zs). Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_comm (xs ys: LinkedList) : append xs ys = append ys xs. Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_cons_r (x: A) (xs ys: LinkedList) : append xs (LCons x ys) = LCons x (append xs ys). Proof. induction xs: simpl: auto. Messages Errors Jobs The term "LinkedList" has type "Type -> Type" which should be Set, Prop or Type.
Can you Fix this error in the following image
Require Import Coq.Lists.List.
Import ListNotations.
Section LinkedList.
Variable A : Type.
Inductive LinkedList :=
| LNil
| LCons (x : A) (xs : LinkedList).
End LinkedList.
Section Append.
Fixpoint append (xs ys : LinkedList) : LinkedList :=
match xs with
| LNil => ys
| LCons x xs' => LCons x (append xs' ys)
end.
End Append.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import tactics.
Section AppendProof.
Context `{!inG Σ (authR (listUR A))}.
Lemma append_nil_r (xs : LinkedList) : append xs LNil = xs.
Proof.
induction xs; simpl; auto.
Qed.
Lemma append_assoc (xs ys zs : LinkedList) :
append (append xs ys) zs = append xs (append ys zs).
Proof.
induction xs; simpl; auto.
rewrite IHxs. reflexivity.
Qed.
Lemma append_comm (xs ys : LinkedList) :
append xs ys = append ys xs.
Proof.
induction xs; simpl; auto.
rewrite IHxs. reflexivity.
Qed.
Lemma append_cons_r (x : A) (xs ys : LinkedList) :
append xs (LCons x ys) = LCons x (append xs ys).
Proof.
induction xs; simpl; auto.
Qed.
End AppendProof.
Step by step
Solved in 2 steps