(* Was an anomaly with ill-typed template polymorphism *) Definition huh (b:bool) := if b thenSetelse Prop. Definition lol b: huh b := if b return huh b then nat else True. Goal (lol true) * unit.
Fail generalize true. (* should fail with error, not anomaly *) Abort.
Messung V0.5
[ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
]
