|
(* Testing robustness of typing for a fixpoint with evars in its type *)
Inductive foo (n : nat) : Type := .
Definition foo_denote {n} (x : foo n) : Type := match x with end.
Definition baz : forall n (x : foo n), foo_denote x.
refine (fix go n (x : foo n) : foo_denote x := _).
Abort.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.25Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
