Commit af840414 authored by Adam Chlipala's avatar Adam Chlipala

Pass through Generic, to incorporate new coqdoc features

parent 4035dcf8
...@@ -360,6 +360,10 @@ Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => ...@@ -360,6 +360,10 @@ Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
]] ]]
*) *)
(* begin hide *)
Definition append' := append.
(* end hide *)
(** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *) (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
...@@ -642,6 +646,10 @@ Theorem map_id : forall T dt ...@@ -642,6 +646,10 @@ Theorem map_id : forall T dt
induction r; crush. induction r; crush.
(* begin hide *)
Definition pred' := pred.
(* end hide *)
(** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments). (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments).
[[ [[
H : forall i : fin (S n), H : forall i : fin (S n),
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment