From Corelib Require Program .Wf.Section Scope .local ] Coercion nat_of_bool (b: bool) : nat :=if b then 0 else 1.Check (refl_equal : true = 0 :> nat).End Scope .Check 0 = true :> nat.Definition ι T (x: T) := x.Check ι _ ι.Definition ιι T (x: T) := x.Check ιι _ ιι.program ]Fixpoint f (n: nat) {wf lt n} : nat := _.program =yes]Fixpoint f (n: nat) {wf lt n} : nat := _."8.9.0" )]Ltac foo := foo.Module M.local ] #[universes(polymorphic)] Definition zed := Type .local , universes(polymorphic)] Definition kats := Type .End M.Check M.zed@{_}.Check zed.Check M.kats@{_}.Check kats.Export Set Foo.export ] Set Foo.export ] Export Foo.(* Attribute for Locality specified twice *) (* Tests for deprecated attribute syntax *) Set Warnings "-deprecated-attribute-syntax" .program =yes]Fixpoint f (n: nat) {wf lt n} : nat := _.Definition ιιι T (x: T) := x.Check ιιι _ ιιι.quality 99%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
