Last active
December 31, 2015 00:59
-
-
Save amutake/7910653 to your computer and use it in GitHub Desktop.
Anomaly: Not enough components to build the dependent tuple. Please report.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Inductive A : Set := a : A. | |
| Definition fantom (n : nat) := A. | |
| Definition fantom_succ {n : nat} : fantom n -> fantom (S n) := | |
| fun _ => a. | |
| Inductive ty : forall n : nat, fantom n -> Prop := | |
| | zero : ty O a | |
| | succ : forall (x : nat) (f : fantom x), ty x f -> ty (S x) (fantom_succ f). | |
| Goal forall (n : nat) (f : fantom n), ty n f -> f = a. | |
| Proof. | |
| intros. | |
| inversion H. (* => Anomaly: Not enough components to build the dependent tuple. Please report. *) | |
| Admitted. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % coqtop --version | |
| The Coq Proof Assistant, version 8.4pl2 (November 2013) | |
| compiled on Nov 29 2013 13:24:57 with OCaml 4.01.0 |
Inductive A : Set := a : A.
Definition fantom (n : nat) := A.
Inductive ty : forall n, fantom n -> Prop :=
| zero : ty O a.
Goal forall (n : nat) (f : fantom n), ty n f -> f = a.
Proof.
intros.
inversion H.
Admitted.これでもなる
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
A の型を Type にすると inversion は通る