|
(*Suppose we have*)
Inductive my_if {A B} : bool -> Type :=
| then_case (_ : A) : my_if true
| else_case (_ : B) : my_if false.
Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10).
(*then here are three inductive type declarations that work:*)
Inductive I1 :=
| i1 (x : I1).
Inductive I2 :=
| i2 (x : nat).
Inductive I3 :=
| i3 (b : bool) (x : If b Then I3 Else nat).
(*and here is one that does not, despite being equivalent to [I3]:*)
Fail Inductive I4 :=
| i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in
"forall b : bool, (if b then I4 else nat) -> I4". *)
(*I think this one should work. I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*)
¤ Dauer der Verarbeitung: 0.116 Sekunden
(vorverarbeitet)
¤
|
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.
|
