| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/success/ (Algebra von RWTH Aachen Version 4.15.1©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle change_pattern.v Sprache: Coq |
|||||||||
|
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.2 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28