|
Set Implicit Arguments.
Unset Strict Implicit.
Axiom vector : Type -> nat -> Type.
Record KleeneStore i j a := kleeneStore
{ dim : nat
; peek : vector j dim -> a
; pos : vector i dim
}.
Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b :=
kleeneStore (fun v => f (peek v)) (pos s).
Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg
{ coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }.
Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x).
Axiom t : Type -> Type.
Axiom traverse : KleeneCoalg (fun x => x) t.
Definition size a (x:t a) : nat := dim (traverse a a x).
Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False.
Proof.
destruct y.
pose (X := KSmap (traverse a unit) (traverse unit a x)).
set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))).
clearbody e.
(** The pattern generated by change must have holes where there were implicit
arguments in the original user-provided term. This particular example fails
if this is not the case because the inferred argument does not coincide with
the one in the considered term. *)
progress (change (dim (traverse unit a x)) with (dim X) in e).
Abort.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
