(* Examples matching fix/cofix in Ltac pattern-matching *)
Goal True.
lazymatch (eval cbv delta [Nat.add] in Nat.add) with
| (fix F (n : nat) (v : ?A) {struct n} : @?P n v
:= match n with
| O => @?O_case v
| S n' => @?S_case n' v F end)
=>
unify A nat;
unify P (fun _ _ : nat => nat);
unify O_case (fun v : nat => v);
unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat)
=> S (add p m)) end. Abort.
Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end.
Goal True.
lazymatch (eval cbv delta [f] in f) with
| fix myf (l : ?L) (n : ?N) {struct n} : nat := match n as _ with
| 0 => ?Z
| S n0 => @?S myf myg n0 l end with myg (n' : ?N') (l' : ?L') {struct n'} : nat := match n' as _ with
| 0 => ?Z'
| S n0' => @?S' myf myg n0' l' end
for myf =>
unify L (list nat);
unify L' (list nat);
unify N nat;
unify N' nat;
unify Z 0;
unify Z' 1;
unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l));
unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n) end.
CoFixpoint f' n l := C1 n (g' (cons n l) n n) with g' l n p := C2 true (f' (S n) l).
Goal True.
lazymatch (eval cbv delta [f'] in f') with
| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l'
for myf =>
unify L (list nat);
unify L' (list nat);
unify N nat;
unify N' nat;
unify N'' nat;
unify T S1;
unify T' S2;
unify X (fun n g l => C1 n (g (cons n l) n n));
unify X' (fun n f (l : list nat) => C2 true (f (S n) l)) end.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
