
products/sources/formale sprachen/Coq/test-suite/bugs/closed/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4157.v Sprache: Coq

Original von: Coq^©

(** The following proof is due to a bug in `vm_compute` and was found by
    Maxime Dénès and Pierre-Marie Pédrot. *)
Inductive t :=
| C_0 : nat -> t
| C_1 : nat -> t
| C_2 : nat -> t
| C_3 : nat -> t
| C_4 : nat -> t
| C_5 : nat -> t
| C_6 : nat -> t
| C_7 : nat -> t
| C_8 : nat -> t
| C_9 : nat -> t
| C_10 : nat -> t
| C_11 : nat -> t
| C_12 : nat -> t
| C_13 : nat -> t
| C_14 : nat -> t
| C_15 : nat -> t
| C_16 : nat -> t
| C_17 : nat -> t
| C_18 : nat -> t
| C_19 : nat -> t
| C_20 : nat -> t
| C_21 : nat -> t
| C_22 : nat -> t
| C_23 : nat -> t
| C_24 : nat -> t
| C_25 : nat -> t
| C_26 : nat -> t
| C_27 : nat -> t
| C_28 : nat -> t
| C_29 : nat -> t
| C_30 : nat -> t
| C_31 : nat -> t
| C_32 : nat -> t
| C_33 : nat -> t
| C_34 : nat -> t
| C_35 : nat -> t
| C_36 : nat -> t
| C_37 : nat -> t
| C_38 : nat -> t
| C_39 : nat -> t
| C_40 : nat -> t
| C_41 : nat -> t
| C_42 : nat -> t
| C_43 : nat -> t
| C_44 : nat -> t
| C_45 : nat -> t
| C_46 : nat -> t
| C_47 : nat -> t
| C_48 : nat -> t
| C_49 : nat -> t
| C_50 : nat -> t
| C_51 : nat -> t
| C_52 : nat -> t
| C_53 : nat -> t
| C_54 : nat -> t
| C_55 : nat -> t
| C_56 : nat -> t
| C_57 : nat -> t
| C_58 : nat -> t
| C_59 : nat -> t
| C_60 : nat -> t
| C_61 : nat -> t
| C_62 : nat -> t
| C_63 : nat -> t
| C_64 : nat -> t
| C_65 : nat -> t
| C_66 : nat -> t
| C_67 : nat -> t
| C_68 : nat -> t
| C_69 : nat -> t
| C_70 : nat -> t
| C_71 : nat -> t
| C_72 : nat -> t
| C_73 : nat -> t
| C_74 : nat -> t
| C_75 : nat -> t
| C_76 : nat -> t
| C_77 : nat -> t
| C_78 : nat -> t
| C_79 : nat -> t
| C_80 : nat -> t
| C_81 : nat -> t
| C_82 : nat -> t
| C_83 : nat -> t
| C_84 : nat -> t
| C_85 : nat -> t
| C_86 : nat -> t
| C_87 : nat -> t
| C_88 : nat -> t
| C_89 : nat -> t
| C_90 : nat -> t
| C_91 : nat -> t
| C_92 : nat -> t
| C_93 : nat -> t
| C_94 : nat -> t
| C_95 : nat -> t
| C_96 : nat -> t
| C_97 : nat -> t
| C_98 : nat -> t
| C_99 : nat -> t
| C_100 : nat -> t
| C_101 : nat -> t
| C_102 : nat -> t
| C_103 : nat -> t
| C_104 : nat -> t
| C_105 : nat -> t
| C_106 : nat -> t
| C_107 : nat -> t
| C_108 : nat -> t
| C_109 : nat -> t
| C_110 : nat -> t
| C_111 : nat -> t
| C_112 : nat -> t
| C_113 : nat -> t
| C_114 : nat -> t
| C_115 : nat -> t
| C_116 : nat -> t
| C_117 : nat -> t
| C_118 : nat -> t
| C_119 : nat -> t
| C_120 : nat -> t
| C_121 : nat -> t
| C_122 : nat -> t
| C_123 : nat -> t
| C_124 : nat -> t
| C_125 : nat -> t
| C_126 : nat -> t
| C_127 : nat -> t
| C_128 : nat -> t
| C_129 : nat -> t
| C_130 : nat -> t
| C_131 : nat -> t
| C_132 : nat -> t
| C_133 : nat -> t
| C_134 : nat -> t
| C_135 : nat -> t
| C_136 : nat -> t
| C_137 : nat -> t
| C_138 : nat -> t
| C_139 : nat -> t
| C_140 : nat -> t
| C_141 : nat -> t
| C_142 : nat -> t
| C_143 : nat -> t
| C_144 : nat -> t
| C_145 : nat -> t
| C_146 : nat -> t
| C_147 : nat -> t
| C_148 : nat -> t
| C_149 : nat -> t
| C_150 : nat -> t
| C_151 : nat -> t
| C_152 : nat -> t
| C_153 : nat -> t
| C_154 : nat -> t
| C_155 : nat -> t
| C_156 : nat -> t
| C_157 : nat -> t
| C_158 : nat -> t
| C_159 : nat -> t
| C_160 : nat -> t
| C_161 : nat -> t
| C_162 : nat -> t
| C_163 : nat -> t
| C_164 : nat -> t
| C_165 : nat -> t
| C_166 : nat -> t
| C_167 : nat -> t
| C_168 : nat -> t
| C_169 : nat -> t
| C_170 : nat -> t
| C_171 : nat -> t
| C_172 : nat -> t
| C_173 : nat -> t
| C_174 : nat -> t
| C_175 : nat -> t
| C_176 : nat -> t
| C_177 : nat -> t
| C_178 : nat -> t
| C_179 : nat -> t
| C_180 : nat -> t
| C_181 : nat -> t
| C_182 : nat -> t
| C_183 : nat -> t
| C_184 : nat -> t
| C_185 : nat -> t
| C_186 : nat -> t
| C_187 : nat -> t
| C_188 : nat -> t
| C_189 : nat -> t
| C_190 : nat -> t
| C_191 : nat -> t
| C_192 : nat -> t
| C_193 : nat -> t
| C_194 : nat -> t
| C_195 : nat -> t
| C_196 : nat -> t
| C_197 : nat -> t
| C_198 : nat -> t
| C_199 : nat -> t
| C_200 : nat -> t
| C_201 : nat -> t
| C_202 : nat -> t
| C_203 : nat -> t
| C_204 : nat -> t
| C_205 : nat -> t
| C_206 : nat -> t
| C_207 : nat -> t
| C_208 : nat -> t
| C_209 : nat -> t
| C_210 : nat -> t
| C_211 : nat -> t
| C_212 : nat -> t
| C_213 : nat -> t
| C_214 : nat -> t
| C_215 : nat -> t
| C_216 : nat -> t
| C_217 : nat -> t
| C_218 : nat -> t
| C_219 : nat -> t
| C_220 : nat -> t
| C_221 : nat -> t
| C_222 : nat -> t
| C_223 : nat -> t
| C_224 : nat -> t
| C_225 : nat -> t
| C_226 : nat -> t
| C_227 : nat -> t
| C_228 : nat -> t
| C_229 : nat -> t
| C_230 : nat -> t
| C_231 : nat -> t
| C_232 : nat -> t
| C_233 : nat -> t
| C_234 : nat -> t
| C_235 : nat -> t
| C_236 : nat -> t
| C_237 : nat -> t
| C_238 : nat -> t
| C_239 : nat -> t
| C_240 : nat -> t
| C_241 : nat -> t
| C_242 : nat -> t
| C_243 : nat -> t
| C_244 : nat -> t
| C_245 : nat -> t
| C_246 : nat -> t
| C_247 : nat -> t
| C_248 : nat -> t
| C_249 : nat -> t
| C_250 : nat -> t
| C_251 : nat -> t
| C_252 : nat -> t
| C_253 : nat -> t
| C_254 : nat -> t
| C_255 : nat -> t
| C_256 : nat -> t.

Definition is_256 (x : t) : bool :=
  match x with
  | C_256 _ => true
  | _ => false
  end.

Lemma falso : False.
  assert (is_256 (C_256 0) = true) by reflexivity.
  (* The next line was successful in 8.2pl3 *)
  Fail assert (is_256 (C_256 0) = false) by (vm_compute; reflexivity).
Abort.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bot Zugriff