pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Scope fix for new N support

Browse source
This commit is contained in:
Adam Chlipala 2020-02-08 15:18:00 -05:00
parent c611524a96
commit f049d7e824
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
FrapWithoutSets.v
View file

@ -431,7 +431,7 @@ Ltac dep_cases E :=
(** * More with [N] *) (** * More with [N] *)
Lemma recursion_step: forall {A: Type} (a: A) (f: N -> A -> A) (n: N), Lemma recursion_step: forall {A: Type} (a: A) (f: N -> A -> A) (n: N),
N.recursion a f (n + 1) = f n (N.recursion a f n). N.recursion a f (n + 1)%N = f n (N.recursion a f n).
Proof. Proof.
intros until f. setoid_rewrite N.add_1_r. intros until f. setoid_rewrite N.add_1_r.
eapply N.recursion_succ; cbv; intuition congruence. eapply N.recursion_succ; cbv; intuition congruence.
@ -459,7 +459,7 @@ Ltac unfold_recurse f k :=
lazymatch rhs with lazymatch rhs with
| N.recursion ?base ?step => | N.recursion ?base ?step =>
let g := eval cbv beta in (step k (f k)) in let g := eval cbv beta in (step k (f k)) in
rewrite (recursion_step base step k : f (k + 1) = g) in * rewrite (recursion_step base step k : f (k + 1)%N = g) in *
| _ => let expected := open_constr:(N.recursion _ _) in | _ => let expected := open_constr:(N.recursion _ _) in
fail "The provided term" f "expands to" rhs "which is not of the expected form" expected fail "The provided term" f "expands to" rhs "which is not of the expected form" expected
end. end.