blob: bd20d9c80409f374140bebfb13862fb639367bfe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
Print Typing Flags.
Unset Guard Checking.
Fixpoint f' (n : nat) : nat := f' n.
Fixpoint f (n : nat) : nat.
Proof.
exact (f n).
Defined.
Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end.
Print Typing Flags.
Set Guard Checking.
Print Assumptions f.
Unset Universe Checking.
Definition T := Type.
Fixpoint g (n : nat) : T := T.
Print Typing Flags.
Set Universe Checking.
Fail Definition g2 (n : nat) : T := T.
Fail Definition e := fix e (n : nat) : nat := e n.
Unset Positivity Checking.
Inductive Cor :=
| Over : Cor
| Next : ((Cor -> list nat) -> list nat) -> Cor.
Set Positivity Checking.
Print Assumptions Cor.
Inductive Box :=
| box : forall n, f n = n -> g 2 -> Box.
Print Assumptions Box.
|
