Created
May 14, 2019 10:24
-
-
Save ichistmeinname/7846aa569c6910db1a6b7e427ebef06e to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* The following two examples fulfill the (strict) positivity condition *) | |
| Inductive Switch (A : Type) : Type := | |
| | switch : Switch A -> Switch A. | |
| Inductive UseSwitch := | |
| | useSwitch : Switch UseSwitch -> UseSwitch. | |
| Inductive SwitchSP (A : Type) : Type := | |
| | switchSP : bool -> SwitchSP A. | |
| Inductive UseSwitchSP := | |
| | useSwitchSP : SwitchSP UseSwitchSP -> UseSwitchSP. | |
| (* this definition, however, does not -- | |
| which rule applies for this definition? | |
| https://coq.inria.fr/refman/language/cic.html#strict-positivity | |
| *) | |
| Inductive SwitchNSP (A : Type) : Type := | |
| | switchNSP : SwitchNSP bool -> SwitchNSP A. | |
| Fail Inductive UseSwitchNSP := | |
| | useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment