forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LamSF_Terms.glob
137 lines (137 loc) · 4.85 KB
/
LamSF_Terms.glob
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
DIGEST eae33cddbc849d74c6ebca0f8f64ca71
FLamSF_Terms
R2283:2287 Coq.Arith.Arith <> <> lib
R2305:2311 General <> <> lib
R2329:2332 Test <> <> lib
ind 2413:2420 <> operator
constr 2428:2430 <> Sop
constr 2435:2437 <> Fop
R2431:2431 LamSF_Terms <> operator ind
R2438:2438 LamSF_Terms <> operator ind
ind 2453:2457 <> lamSF
constr 2472:2474 <> Ref
constr 2496:2497 <> Op
constr 2525:2527 <> Abs
constr 2552:2554 <> App
R2481:2484 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2485:2489 LamSF_Terms <> lamSF ind
R2478:2480 Coq.Init.Datatypes <> nat ind
R2510:2513 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2514:2518 LamSF_Terms <> lamSF ind
R2502:2509 LamSF_Terms <> operator ind
R2536:2539 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2540:2544 LamSF_Terms <> lamSF ind
R2531:2535 LamSF_Terms <> lamSF ind
R2563:2566 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2572:2575 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2576:2580 LamSF_Terms <> lamSF ind
R2567:2571 LamSF_Terms <> lamSF ind
R2558:2562 LamSF_Terms <> lamSF ind
prf 2591:2613 <> decidable_term_equality
R2630:2634 LamSF_Terms <> lamSF ind
R2643:2646 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R2639:2641 Coq.Init.Logic <> :type_scope:x_'='_x not
R2638:2638 LamSF_Terms <> M var
R2642:2642 LamSF_Terms <> N var
R2648:2650 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R2647:2647 LamSF_Terms <> M var
R2651:2651 LamSF_Terms <> N var
R2751:2764 General <> decidable_nats thm
R2751:2764 General <> decidable_nats thm
def 3073:3080 <> relocate
R3091:3093 Coq.Init.Datatypes <> nat ind
R3107:3110 Test <> test def
R3114:3114 LamSF_Terms <> i var
R3112:3112 LamSF_Terms <> k var
R3143:3146 Coq.Init.Specif <> left constr
R3154:3154 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3153:3153 LamSF_Terms <> n var
R3155:3155 LamSF_Terms <> i var
R3178:3178 LamSF_Terms <> i var
def 3197:3204 <> lift_rec
R3211:3215 LamSF_Terms <> lamSF ind
R3223:3226 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3230:3233 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3234:3238 LamSF_Terms <> lamSF ind
R3227:3229 Coq.Init.Datatypes <> nat ind
R3220:3222 Coq.Init.Datatypes <> nat ind
R3265:3265 LamSF_Terms <> L var
R3276:3278 LamSF_Terms <> Ref constr
R3285:3287 LamSF_Terms <> Ref constr
R3290:3297 LamSF_Terms <> relocate def
R3303:3303 LamSF_Terms <> n var
R3301:3301 LamSF_Terms <> k var
R3310:3311 LamSF_Terms <> Op constr
R3318:3319 LamSF_Terms <> Op constr
R3327:3329 LamSF_Terms <> App constr
R3338:3340 LamSF_Terms <> App constr
R3360:3367 LamSF_Terms <> lift_rec def
R3373:3373 LamSF_Terms <> n var
R3371:3371 LamSF_Terms <> k var
R3343:3350 LamSF_Terms <> lift_rec def
R3356:3356 LamSF_Terms <> n var
R3354:3354 LamSF_Terms <> k var
R3380:3382 LamSF_Terms <> Abs constr
R3389:3391 LamSF_Terms <> Abs constr
R3394:3401 LamSF_Terms <> lift_rec def
R3411:3411 LamSF_Terms <> n var
R3406:3406 Coq.Init.Datatypes <> S constr
R3408:3408 LamSF_Terms <> k var
def 3433:3436 <> lift
R3443:3445 Coq.Init.Datatypes <> nat ind
R3453:3457 LamSF_Terms <> lamSF ind
R3463:3470 LamSF_Terms <> lift_rec def
R3476:3476 LamSF_Terms <> n var
R3472:3472 LamSF_Terms <> N var
def 3512:3521 <> insert_Ref
R3528:3532 LamSF_Terms <> lamSF ind
R3542:3544 Coq.Init.Datatypes <> nat ind
R3558:3564 Test <> compare def
R3568:3568 LamSF_Terms <> i var
R3566:3566 LamSF_Terms <> k var
R3593:3598 Coq.Init.Specif <> inleft constr
R3601:3604 Coq.Init.Specif <> left constr
R3612:3614 LamSF_Terms <> Ref constr
R3617:3620 Coq.Init.Peano <> pred syndef
R3622:3622 LamSF_Terms <> i var
R3640:3645 Coq.Init.Specif <> inleft constr
R3652:3655 LamSF_Terms <> lift def
R3659:3659 LamSF_Terms <> N var
R3657:3657 LamSF_Terms <> k var
R3681:3683 LamSF_Terms <> Ref constr
R3685:3685 LamSF_Terms <> i var
def 3704:3712 <> subst_rec
R3719:3723 LamSF_Terms <> lamSF ind
R3733:3736 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3740:3743 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3744:3748 LamSF_Terms <> lamSF ind
R3737:3739 Coq.Init.Datatypes <> nat ind
R3728:3732 LamSF_Terms <> lamSF ind
R3764:3768 LamSF_Terms <> lamSF ind
R3776:3778 Coq.Init.Datatypes <> nat ind
R3792:3792 LamSF_Terms <> L var
R3803:3805 LamSF_Terms <> Ref constr
R3812:3821 LamSF_Terms <> insert_Ref def
R3827:3827 LamSF_Terms <> k var
R3823:3823 LamSF_Terms <> N var
R3833:3834 LamSF_Terms <> Op constr
R3841:3842 LamSF_Terms <> Op constr
R3850:3852 LamSF_Terms <> App constr
R3862:3864 LamSF_Terms <> App constr
R3885:3893 LamSF_Terms <> subst_rec def
R3900:3900 LamSF_Terms <> k var
R3898:3898 LamSF_Terms <> N var
R3867:3875 LamSF_Terms <> subst_rec def
R3881:3881 LamSF_Terms <> k var
R3879:3879 LamSF_Terms <> N var
R3907:3909 LamSF_Terms <> Abs constr
R3916:3918 LamSF_Terms <> Abs constr
R3921:3929 LamSF_Terms <> subst_rec def
R3936:3936 Coq.Init.Datatypes <> S constr
R3938:3938 LamSF_Terms <> k var
R3933:3933 LamSF_Terms <> N var
def 3962:3966 <> subst
R3975:3979 LamSF_Terms <> lamSF ind
R3985:3993 LamSF_Terms <> subst_rec def
R3997:3997 LamSF_Terms <> N var
R3995:3995 LamSF_Terms <> M var