stlc.html

Filter predicate:

File "coq-builtin.elpi: default-declare-evar", line 268, column 0, character 10808:
declare_constraint (declare-evar Ctx RawEv Ty Ev)
[
RawEv
]
declare-evar Ctx RawEv Ty Ev
File "coq-builtin.elpi", line 277, column 0, character 11168:
declare_constraint (rm-evar X Y)
[
X,
Y
]
rm-evar
(uvar as 
X)
(uvar as 
Y)
File "coq-builtin.elpi", line 278, column 0, character 11245:
rm-evar _ _
File "coq-builtin.elpi", line 299, column 0, character 12025:
var S _ VL,
!,
prune T VL,
prune X VL,
declare_constraint (evar X T S)
[
X,
S
]
evar
(uvar as 
X)
T S
File "coq-builtin.elpi: default-assign-evar", line 302, column 0, character 12131:
evar _ _ _
File "coq-builtin.elpi", line 747, column 3, character 30685:
coq.warning elpi.deprecated elpi.const-opaque use coq.env.opaque? in place of coq.env.const-opaque?,
coq.env.opaque? C
coq.env.const-opaque? C
File "coq-builtin.elpi", line 754, column 3, character 30933:
coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?,
coq.env.primitive? C
coq.env.const-primitive? C
File "coq-builtin.elpi", line 835, column 0, character 34271:
coq.env.begin-module-functor Name MP []
coq.env.begin-module Name MP
File "coq-builtin.elpi", line 848, column 0, character 34752:
coq.env.begin-module-type-functor Name []
coq.env.begin-module-type Name
File "coq-builtin.elpi", line 1211, column 0, character 48987:
coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,
coq.env.projections I L
coq.CS.canonical-projections I L
File "coq-builtin.elpi", line 1514, column 0, character 61760:
coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,
coq.reduction.cbv.norm T R
coq.reduction.cbv.whd_all T R
File "coq-builtin.elpi", line 1521, column 0, character 62038:
coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,
coq.reduction.vm.norm T TY R
coq.reduction.vm.whd_all T TY R
File "coq-builtin.elpi", line 1528, column 0, character 62272:
get-option coq:redflags coq.redflags.all ⇒ 
coq.reduction.lazy.whd X Y
coq.reduction.lazy.whd_all X Y
File "coq-builtin.elpi", line 1645, column 0, character 66783:
coq.string->name S N
coq.id->name S N
File "coq-builtin.elpi", line 1746, column 0, character 70529:
coq.elpi.accumulate-clauses S N
[
C
]
coq.elpi.accumulate S N C
File "elpi-builtin.elpi", line 9, column 0, character 89:
true
File "elpi-builtin.elpi", line 28, column 0, character 296:
A
(A ; 
_)
File "elpi-builtin.elpi", line 30, column 0, character 311:
B
(_ ; 
B)
File "elpi-builtin.elpi", line 52, column 0, character 609:
X,
!,
fail
not X
File "elpi-builtin.elpi", line 54, column 0, character 631:
not _
File "elpi-builtin.elpi", line 67, column 0, character 974:
halt
stop
File "elpi-builtin.elpi", line 73, column 0, character 1031:
calc Y X
X is 
Y
File "elpi-builtin.elpi", line 173, column 0, character 2867:
gt_ X Y
> X Y
File "elpi-builtin.elpi", line 175, column 0, character 2888:
lt_ X Y
X < 
Y
File "elpi-builtin.elpi", line 177, column 0, character 2909:
le_ X Y
=< X Y
File "elpi-builtin.elpi", line 179, column 0, character 2930:
ge_ X Y
>= X Y
File "elpi-builtin.elpi", line 183, column 0, character 3002:
lt_ X Y
i< X Y
File "elpi-builtin.elpi", line 185, column 0, character 3023:
gt_ X Y
i> X Y
File "elpi-builtin.elpi", line 187, column 0, character 3044:
le_ X Y
i=< X Y
File "elpi-builtin.elpi", line 189, column 0, character 3065:
ge_ X Y
i>= X Y
File "elpi-builtin.elpi", line 193, column 0, character 3141:
lt_ X Y
r< X Y
File "elpi-builtin.elpi", line 195, column 0, character 3162:
gt_ X Y
r> X Y
File "elpi-builtin.elpi", line 197, column 0, character 3183:
le_ X Y
r=< X Y
File "elpi-builtin.elpi", line 199, column 0, character 3204:
ge_ X Y
r>= X Y
File "elpi-builtin.elpi", line 203, column 0, character 3282:
lt_ X Y
s< X Y
File "elpi-builtin.elpi", line 205, column 0, character 3303:
gt_ X Y
s> X Y
File "elpi-builtin.elpi", line 207, column 0, character 3324:
le_ X Y
s=< X Y
File "elpi-builtin.elpi", line 209, column 0, character 3345:
ge_ X Y
s>= X Y
File "elpi-builtin.elpi", line 230, column 0, character 3755:
fst (pr A _) A
File "elpi-builtin.elpi", line 234, column 0, character 3800:
snd (pr _ B) B
File "elpi-builtin.elpi", line 262, column 0, character 4438:
trace.counter C N
counter C N
File "elpi-builtin.elpi", line 293, column 0, character 5594:
rex.match Rx S
rex_match Rx S
File "elpi-builtin.elpi", line 297, column 0, character 5716:
rex.replace Rx R S O
rex_replace Rx R S O
File "elpi-builtin.elpi", line 301, column 0, character 5841:
rex.split Rx S L
rex_split Rx S L
File "elpi-builtin.elpi", line 335, column 0, character 7069:
same_term X Y
== X Y
File "elpi-builtin.elpi", line 369, column 0, character 8255:
is_cdata X (ctype S)
primitive? X S
File "elpi-builtin.elpi", line 400, column 0, character 9220:
B,
!,
T
if B T _
File "elpi-builtin.elpi", line 401, column 0, character 9241:
E
if _ _ E
File "elpi-builtin.elpi", line 405, column 0, character 9384:
G1,
!,
P1
if2 G1 P1 _ _ _
File "elpi-builtin.elpi", line 406, column 0, character 9416:
G2,
!,
P2
if2 _ _ G2 P2 _
File "elpi-builtin.elpi", line 407, column 0, character 9448:
E
if2 _ _ _ _ E
File "builtin_stdlib.elpi: default-fatal-error", line 16, column 0, character 659:
halt Msg
std.fatal-error Msg
File "builtin_stdlib.elpi: default-fatal-error-w-data", line 20, column 0, character 756:
halt Msg : Data
std.fatal-error-w-data Msg Data
File "builtin_stdlib.elpi: default-debug-print", line 24, column 0, character 874:
print Msg Data
std.debug-print Msg Data
File "builtin_stdlib.elpi", line 30, column 0, character 1007:
P,
!
std.ignore-failure! P
File "builtin_stdlib.elpi", line 31, column 0, character 1034:
std.ignore-failure! _
File "builtin_stdlib.elpi", line 35, column 0, character 1155:
(Cond ; 
std.fatal-error-w-data Msg Cond),
!
std.assert! Cond Msg
File "builtin_stdlib.elpi", line 40, column 0, character 1406:
Cond Diagnostic,
!,
(Diagnostic = 
ok ; 
Diagnostic = 
(error S),
std.fatal-error-w-data Msg S),
!
std.assert-ok! Cond Msg
File "builtin_stdlib.elpi", line 41, column 0, character 1520:
std.fatal-error-w-data Msg no diagnostic returned
std.assert-ok! _ Msg
File "builtin_stdlib.elpi", line 45, column 0, character 1682:
trace.counter run NR,
if (not
(NR = 
0))
(std.debug-print run= NR) true,
std.debug-print ----<<---- enter: P,
P,
std.debug-print ---->>---- exit: P
std.spy P
File "builtin_stdlib.elpi", line 49, column 0, character 1863:
std.debug-print ---->>---- fail: P,
fail
std.spy P
File "builtin_stdlib.elpi", line 53, column 0, character 2001:
trace.counter run NR,
if (not
(NR = 
0))
(std.debug-print run= NR) true,
std.debug-print ----<<---- enter: P,
P,
std.debug-print ---->>---- exit: P,
!
std.spy! P
File "builtin_stdlib.elpi", line 57, column 0, character 2186:
std.debug-print ---->>---- fail: P,
fail
std.spy! P
File "builtin_stdlib.elpi", line 61, column 0, character 2295:
std.unsafe-cast X X
File "builtin_stdlib.elpi", line 66, column 0, character 2367:
std.length L N1,
N is 
N1 + 
1
std.length
[
_ | L
]
N
File "builtin_stdlib.elpi", line 67, column 0, character 2411:
std.length [] 0
File "builtin_stdlib.elpi", line 70, column 0, character 2457:
std.rev.aux L [] RL
std.rev L RL
File "builtin_stdlib.elpi", line 71, column 0, character 2488:
std.rev.aux XS
[
X | ACC
]
R
std.rev.aux
[
X | XS
]
ACC R
File "builtin_stdlib.elpi", line 72, column 0, character 2534:
std.rev.aux [] L L
File "builtin_stdlib.elpi", line 75, column 0, character 2576:
std.fatal-error last on empty list
std.last [] _
File "builtin_stdlib.elpi", line 76, column 0, character 2623:
!
std.last
[
X
]
X
File "builtin_stdlib.elpi", line 77, column 0, character 2640:
std.last XS R
std.last
[
_ | XS
]
R
File "builtin_stdlib.elpi", line 80, column 0, character 2711:
std.append XS L L1
std.append
[
X | XS
]
L
[
X | L1
]
File "builtin_stdlib.elpi", line 81, column 0, character 2754:
std.append [] L L
File "builtin_stdlib.elpi", line 84, column 0, character 2814:
std.appendR XS L L1
std.appendR
[
X | XS
]
L
[
X | L1
]
File "builtin_stdlib.elpi", line 85, column 0, character 2859:
std.appendR [] L L
File "builtin_stdlib.elpi", line 88, column 0, character 2914:
!
std.take 0 _ []
File "builtin_stdlib.elpi", line 89, column 0, character 2932:
N1 is 
- N 1,
std.take N1 XS L
std.take N
[
X | XS
]
[
X | L
]
File "builtin_stdlib.elpi", line 90, column 0, character 2985:
std.fatal-error take run out of list items
std.take _ _ _
File "builtin_stdlib.elpi", line 93, column 0, character 3084:
std.length L M,
D is 
- M N,
std.drop D L R
std.take-last N L R
File "builtin_stdlib.elpi", line 99, column 0, character 3183:
!
std.drop 0 L L
File "builtin_stdlib.elpi", line 100, column 0, character 3200:
N1 is 
- N 1,
std.drop N1 XS L
std.drop N
[
_ | XS
]
L
File "builtin_stdlib.elpi", line 101, column 0, character 3249:
std.fatal-error drop run out of list items
std.drop _ _ _
File "builtin_stdlib.elpi", line 104, column 0, character 3348:
std.length L M,
I is 
- M N,
std.take I L R
std.drop-last N L R
File "builtin_stdlib.elpi", line 108, column 0, character 3457:
!
std.split-at 0 L [] L
File "builtin_stdlib.elpi", line 109, column 0, character 3481:
N1 is 
- N 1,
std.split-at N1 XS LN LM
std.split-at N
[
X | XS
]
[
X | LN
]
LM
File "builtin_stdlib.elpi", line 110, column 0, character 3550:
std.fatal-error split-at run out of list items
std.split-at _ _ _ _
File "builtin_stdlib.elpi", line 113, column 0, character 3672:
std.fold [] A _ A
File "builtin_stdlib.elpi", line 114, column 0, character 3687:
F X A A1,
std.fold XS A1 F R
std.fold
[
X | XS
]
A F R
File "builtin_stdlib.elpi", line 117, column 0, character 3796:
std.fold-right [] A _ A
File "builtin_stdlib.elpi", line 118, column 0, character 3817:
std.fold-right XS A F A',
F X A' R
std.fold-right
[
X | XS
]
A F R
File "builtin_stdlib.elpi", line 121, column 0, character 3948:
std.fatal-error fold2 on lists of different length
std.fold2 []
[
_ | _
]
_ _ _
File "builtin_stdlib.elpi", line 122, column 0, character 4022:
std.fatal-error fold2 on lists of different length
std.fold2
[
_ | _
]
[] _ _ _
File "builtin_stdlib.elpi", line 123, column 0, character 4096:
std.fold2 [] [] A _ A
File "builtin_stdlib.elpi", line 124, column 0, character 4115:
F X Y A A1,
std.fold2 XS YS A1 F R
std.fold2
[
X | XS
]
[
Y | YS
]
A F R
File "builtin_stdlib.elpi", line 127, column 0, character 4226:
std.map [] _ []
File "builtin_stdlib.elpi", line 128, column 0, character 4239:
F X Y,
std.map XS F YS
std.map
[
X | XS
]
F
[
Y | YS
]
File "builtin_stdlib.elpi", line 131, column 0, character 4341:
std.map-i.aux L 0 F R
std.map-i L F R
File "builtin_stdlib.elpi", line 132, column 0, character 4375:
std.map-i.aux [] _ _ []
File "builtin_stdlib.elpi", line 133, column 0, character 4396:
F N X Y,
M is 
N + 
1,
std.map-i.aux XS M F YS
std.map-i.aux
[
X | XS
]
N F
[
Y | YS
]
File "builtin_stdlib.elpi", line 136, column 0, character 4526:
std.map-filter [] _ []
File "builtin_stdlib.elpi", line 137, column 0, character 4546:
F X Y,
!,
std.map-filter XS F YS
std.map-filter
[
X | XS
]
F
[
Y | YS
]
File "builtin_stdlib.elpi", line 138, column 0, character 4606:
std.map-filter XS F YS
std.map-filter
[
_ | XS
]
F YS
File "builtin_stdlib.elpi", line 142, column 0, character 4730:
std.fatal-error map2 on lists of different length
std.map2 []
[
_ | _
]
_ _
File "builtin_stdlib.elpi", line 143, column 0, character 4800:
std.fatal-error map2 on lists of different length
std.map2
[
_ | _
]
[] _ _
File "builtin_stdlib.elpi", line 144, column 0, character 4870:
std.map2 [] [] _ []
File "builtin_stdlib.elpi", line 145, column 0, character 4887:
F X Y Z,
std.map2 XS YS F ZS
std.map2
[
X | XS
]
[
Y | YS
]
F
[
Z | ZS
]
File "builtin_stdlib.elpi", line 148, column 0, character 5017:
std.fatal-error map2-filter on lists of different length
std.map2-filter []
[
_ | _
]
_ _
File "builtin_stdlib.elpi", line 149, column 0, character 5101:
std.fatal-error map2-filter on lists of different length
std.map2-filter
[
_ | _
]
[] _ _
File "builtin_stdlib.elpi", line 150, column 0, character 5185:
std.map2-filter [] [] _ []
File "builtin_stdlib.elpi", line 151, column 0, character 5209:
F X Y Z,
!,
std.map2-filter XS YS F ZS
std.map2-filter
[
X | XS
]
[
Y | YS
]
F
[
Z | ZS
]
File "builtin_stdlib.elpi", line 152, column 0, character 5283:
std.map2-filter XS YS F ZS
std.map2-filter
[
_ | XS
]
[
_ | YS
]
F ZS
File "builtin_stdlib.elpi", line 155, column 0, character 5422:
P X Y S0,
if
(S0 = 
ok)
(std.map-ok L P YS S)
(S = 
S0)
std.map-ok
[
X | L
]
P
[
Y | YS
]
S
File "builtin_stdlib.elpi", line 156, column 0, character 5500:
std.map-ok [] _ [] ok
File "builtin_stdlib.elpi", line 159, column 0, character 5594:
std.fold-map [] A _ [] A
File "builtin_stdlib.elpi", line 160, column 0, character 5616:
F X A Y A1,
std.fold-map XS A1 F YS A2
std.fold-map
[
X | XS
]
A F
[
Y | YS
]
A2
File "builtin_stdlib.elpi", line 163, column 0, character 5740:
std.omap none _ none
File "builtin_stdlib.elpi", line 164, column 0, character 5758:
F X Y
std.omap (some X) F (some Y)
File "builtin_stdlib.elpi", line 168, column 0, character 5898:
X = 
R
std.nth 0
[
X | _
]
R
File "builtin_stdlib.elpi", line 169, column 0, character 5926:
> N 0,
!,
N1 is 
- N 1,
std.nth N1 XS R
std.nth N
[
_ | XS
]
R
File "builtin_stdlib.elpi", line 170, column 0, character 5980:
N < 
0,
!,
std.fatal-error nth got a negative index
std.nth N _ _
File "builtin_stdlib.elpi", line 171, column 0, character 6043:
std.fatal-error nth run out of list items
std.nth _ _ _
File "builtin_stdlib.elpi", line 175, column 0, character 6184:
std.lookup
[
pr X Y | _
]
X Y
File "builtin_stdlib.elpi", line 176, column 0, character 6207:
std.lookup LS X Y
std.lookup
[
_ | LS
]
X Y
File "builtin_stdlib.elpi", line 180, column 0, character 6366:
!
std.lookup!
[
pr X Y | _
]
X Y
File "builtin_stdlib.elpi", line 181, column 0, character 6395:
std.lookup! LS X Y
std.lookup!
[
_ | LS
]
X Y
File "builtin_stdlib.elpi", line 185, column 0, character 6514:
!
std.mem!
[
X | _
]
X
File "builtin_stdlib.elpi", line 186, column 0, character 6533:
std.mem! L X
std.mem!
[
_ | L
]
X
File "builtin_stdlib.elpi", line 190, column 0, character 6638:
std.mem
[
X | _
]
X
File "builtin_stdlib.elpi", line 191, column 0, character 6651:
std.mem L X
std.mem
[
_ | L
]
X
File "builtin_stdlib.elpi", line 194, column 0, character 6713:
P X
std.exists
[
X | _
]
P
File "builtin_stdlib.elpi", line 195, column 0, character 6736:
std.exists L P
std.exists
[
_ | L
]
P
File "builtin_stdlib.elpi", line 198, column 0, character 6820:
std.fatal-error exists2 on lists of different length
std.exists2 []
[
_ | _
]
_
File "builtin_stdlib.elpi", line 199, column 0, character 6894:
std.fatal-error exists2 on lists of different length
std.exists2
[
_ | _
]
[] _
File "builtin_stdlib.elpi", line 200, column 0, character 6968:
P X Y
std.exists2
[
X | _
]
[
Y | _
]
P
File "builtin_stdlib.elpi", line 201, column 0, character 7000:
std.exists2 L M P
std.exists2
[
_ | L
]
[
_ | M
]
P
File "builtin_stdlib.elpi", line 204, column 0, character 7078:
std.forall [] _
File "builtin_stdlib.elpi", line 205, column 0, character 7091:
P X,
std.forall L P
std.forall
[
X | L
]
P
File "builtin_stdlib.elpi", line 208, column 0, character 7195:
P X S0,
if
(S0 = 
ok)
(std.forall-ok L P S)
(S = 
S0)
std.forall-ok
[
X | L
]
P S
File "builtin_stdlib.elpi", line 209, column 0, character 7267:
std.forall-ok [] _ ok
File "builtin_stdlib.elpi", line 212, column 0, character 7340:
std.fatal-error forall2 on lists of different length
std.forall2 []
[
_ | _
]
_
File "builtin_stdlib.elpi", line 213, column 0, character 7414:
std.fatal-error forall2 on lists of different length
std.forall2
[
_ | _
]
[] _
File "builtin_stdlib.elpi", line 214, column 0, character 7488:
P X Y,
std.forall2 XS YS P
std.forall2
[
X | XS
]
[
Y | YS
]
P
File "builtin_stdlib.elpi", line 215, column 0, character 7539:
std.forall2 [] [] _
File "builtin_stdlib.elpi", line 218, column 0, character 7604:
std.filter [] _ []
File "builtin_stdlib.elpi", line 219, column 0, character 7623:
if (P X)
(R = 
[
X | L1
]
)
(R = 
L1),
std.filter L P L1
std.filter
[
X | L
]
P R
File "builtin_stdlib.elpi", line 222, column 0, character 7740:
std.fatal-error zip on lists of different length
std.zip
[
_ | _
]
[] _
File "builtin_stdlib.elpi", line 223, column 0, character 7806:
std.fatal-error zip on lists of different length
std.zip []
[
_ | _
]
_
File "builtin_stdlib.elpi", line 224, column 0, character 7872:
std.zip LX LY LR
std.zip
[
X | LX
]
[
Y | LY
]
[
pr X Y | LR
]
File "builtin_stdlib.elpi", line 225, column 0, character 7919:
std.zip [] [] []
File "builtin_stdlib.elpi", line 228, column 0, character 7984:
std.unzip [] [] []
File "builtin_stdlib.elpi", line 229, column 0, character 8000:
std.unzip L LX LY
std.unzip
[
pr X Y | L
]
[
X | LX
]
[
Y | LY
]
File "builtin_stdlib.elpi", line 232, column 0, character 8090:
std.flatten LS LS',
std.append X LS' R
std.flatten
[
X | LS
]
R
File "builtin_stdlib.elpi", line 233, column 0, character 8142:
std.flatten [] []
File "builtin_stdlib.elpi", line 236, column 0, character 8182:
std.null []
File "builtin_stdlib.elpi", line 239, column 0, character 8221:
std.iota.aux 0 N L
std.iota N L
File "builtin_stdlib.elpi", line 240, column 0, character 8249:
!
std.iota.aux X X []
File "builtin_stdlib.elpi", line 241, column 0, character 8271:
M is 
N + 
1,
std.iota.aux M X R
std.iota.aux N X
[
N | R
]
File "builtin_stdlib.elpi", line 246, column 0, character 8423:
std.intersperse _ [] []
File "builtin_stdlib.elpi", line 247, column 0, character 8444:
!
std.intersperse _
[
X
]
[
X
]
File "builtin_stdlib.elpi", line 248, column 0, character 8472:
std.intersperse Sep XS YS
std.intersperse Sep
[
X | XS
]
[
X,
Sep | YS
]
File "builtin_stdlib.elpi", line 253, column 0, character 8588:
P Y X
std.flip P X Y
File "builtin_stdlib.elpi", line 256, column 0, character 8637:
gettimeofday Before,
P,
gettimeofday After,
T is 
- After Before
std.time P T
File "builtin_stdlib.elpi", line 259, column 0, character 8737:
std.do! []
File "builtin_stdlib.elpi", line 260, column 0, character 8745:
P,
!,
std.do! PS
std.do!
[
P | PS
]
File "builtin_stdlib.elpi", line 264, column 0, character 8841:
std.do-ok! ok []
File "builtin_stdlib.elpi", line 265, column 0, character 8855:
P S0,
!,
if
(S0 = 
ok)
(std.do-ok! S PS)
(S = 
S0)
std.do-ok! S
[
P | PS
]
File "builtin_stdlib.elpi", line 268, column 0, character 8966:
(P,
R = 
ok ; 
R = 
(error Msg))
std.lift-ok P Msg R
File "builtin_stdlib.elpi", line 271, column 0, character 9040:
std.map L
λx1.
λx2.
x2 = 
(std.spy x1)
L1,
std.do! L1
std.spy-do! L
File "builtin_stdlib.elpi", line 274, column 0, character 9163:
std.while-ok-do!
(error _ as 
E)
_ E
File "builtin_stdlib.elpi", line 275, column 0, character 9196:
std.while-ok-do! ok [] ok
File "builtin_stdlib.elpi", line 276, column 0, character 9219:
P C,
!,
std.while-ok-do! C PS R
std.while-ok-do! ok
[
P | PS
]
R
File "builtin_stdlib.elpi", line 279, column 0, character 9309:
term_to_string X Y
std.any->string X Y
File "builtin_stdlib.elpi", line 282, column 0, character 9373:
>= N M,
!
std.max N M N
File "builtin_stdlib.elpi", line 283, column 0, character 9397:
std.max _ M M
File "builtin_stdlib.elpi", line 287, column 0, character 9520:
findall_solutions P L
std.findall P L
File "builtin_map.elpi", line 7, column 0, character 10094:
std.map.make Cmp (std.map std.map.private.empty Cmp)
File "builtin_map.elpi", line 11, column 0, character 10226:
std.map.private.find M Cmp K V
std.map.find K (std.map M Cmp) V
File "builtin_map.elpi", line 15, column 0, character 10375:
std.map.private.add M Cmp K V M1
std.map.add K V (std.map M Cmp) (std.map M1 Cmp)
File "builtin_map.elpi", line 19, column 0, character 10538:
std.map.private.remove M Cmp K M1
std.map.remove K (std.map M Cmp) (std.map M1 Cmp)
File "builtin_map.elpi", line 23, column 0, character 10721:
std.map.private.bindings M [] L
std.map.bindings (std.map M _) L
File "builtin_map.elpi", line 33, column 0, character 10964:
std.map.private.height std.map.private.empty 0
File "builtin_map.elpi", line 34, column 0, character 10980:
std.map.private.height (std.map.private.node _ _ _ _ H) H
File "builtin_map.elpi", line 37, column 0, character 11063:
std.map.private.height L Spilled1,
std.map.private.height R Spilled2,
std.max Spilled1 Spilled2 Spilled3,
H is 
Spilled3 + 
1
std.map.private.create L K V R (std.map.private.node L K V R H)
File "builtin_map.elpi", line 40, column 0, character 11193:
std.map.private.height L HL,
std.map.private.height R HR,
HL2 is 
HL + 
2,
HR2 is 
HR + 
2,
std.map.private.bal.aux HL HR HL2 HR2 L K V R T
std.map.private.bal L K V R T
File "builtin_map.elpi", line 47, column 0, character 11310:
> HL HR2,
std.map.private.height LL Spilled2,
std.map.private.height LR Spilled3,
>= Spilled2 Spilled3,
!,
std.map.private.create LR X D R Spilled1,
std.map.private.create LL LV LD Spilled1 T
std.map.private.bal.aux HL _ _ HR2 (std.map.private.node LL LV LD LR _) X D R T
File "builtin_map.elpi", line 50, column 0, character 11443:
> HL HR2,
!,
std.map.private.create LL LV LD LRL Spilled1,
std.map.private.create LRR X D R Spilled2,
std.map.private.create Spilled1 LRV LRD Spilled2 T
std.map.private.bal.aux HL _ _ HR2 (std.map.private.node LL LV LD (std.map.private.node LRL LRV LRD LRR _) _) X D R T
File "builtin_map.elpi", line 53, column 0, character 11592:
> HR HL2,
std.map.private.height RR Spilled2,
std.map.private.height RL Spilled3,
>= Spilled2 Spilled3,
!,
std.map.private.create L X D RL Spilled1,
std.map.private.create Spilled1 RV RD RR T
std.map.private.bal.aux _ HR HL2 _ L X D (std.map.private.node RL RV RD RR _) T
File "builtin_map.elpi", line 56, column 0, character 11725:
> HR HL2,
!,
std.map.private.create L X D RLL Spilled1,
std.map.private.create RLR RV RD RR Spilled2,
std.map.private.create Spilled1 RLV RLD Spilled2 T
std.map.private.bal.aux _ HR HL2 _ L X D (std.map.private.node (std.map.private.node RLL RLV RLD RLR _) RV RD RR _) T
File "builtin_map.elpi", line 59, column 0, character 11874:
std.map.private.create L K V R T
std.map.private.bal.aux _ _ _ _ L K V R T
File "builtin_map.elpi", line 62, column 0, character 11990:
std.map.private.create std.map.private.empty K V std.map.private.empty T
std.map.private.add std.map.private.empty _ K V T
File "builtin_map.elpi", line 63, column 0, character 12037:
Cmp X1 X E,
std.map.private.add.aux E M Cmp X1 XD M1
std.map.private.add
(std.map.private.node _ X _ _ _ as 
M)
Cmp X1 XD M1
File "builtin_map.elpi", line 64, column 0, character 12117:
T = 
(std.map.private.node L X XD R H)
std.map.private.add.aux eq (std.map.private.node L _ _ R H) _ X XD T
File "builtin_map.elpi", line 65, column 0, character 12181:
std.map.private.add L Cmp X XD Spilled1,
std.map.private.bal Spilled1 V D R T
std.map.private.add.aux lt (std.map.private.node L V D R _) Cmp X XD T
File "builtin_map.elpi", line 66, column 0, character 12253:
std.map.private.add R Cmp X XD Spilled1,
std.map.private.bal L V D Spilled1 T
std.map.private.add.aux gt (std.map.private.node L V D R _) Cmp X XD T
File "builtin_map.elpi", line 69, column 0, character 12384:
Cmp K K1 E,
std.map.private.find.aux E Cmp L R V1 K V
std.map.private.find (std.map.private.node L K1 V1 R _) Cmp K V
File "builtin_map.elpi", line 70, column 0, character 12458:
std.map.private.find.aux eq _ _ _ V _ V
File "builtin_map.elpi", line 71, column 0, character 12485:
std.map.private.find L Cmp K V
std.map.private.find.aux lt Cmp L _ _ K V
File "builtin_map.elpi", line 72, column 0, character 12530:
std.map.private.find R Cmp K V
std.map.private.find.aux gt Cmp _ R _ K V
File "builtin_map.elpi", line 75, column 0, character 12622:
!
std.map.private.remove-min-binding (std.map.private.node std.map.private.empty _ _ R _) R
File "builtin_map.elpi", line 76, column 0, character 12670:
std.map.private.remove-min-binding L Spilled1,
std.map.private.bal Spilled1 V D R X
std.map.private.remove-min-binding (std.map.private.node L V D R _) X
File "builtin_map.elpi", line 79, column 0, character 12786:
!
std.map.private.min-binding (std.map.private.node std.map.private.empty V D _ _) V D
File "builtin_map.elpi", line 80, column 0, character 12829:
std.map.private.min-binding L V D
std.map.private.min-binding (std.map.private.node L _ _ _ _) V D
File "builtin_map.elpi", line 83, column 0, character 12929:
!
std.map.private.merge std.map.private.empty X X
File "builtin_map.elpi", line 84, column 0, character 12951:
!
std.map.private.merge X std.map.private.empty X
File "builtin_map.elpi", line 85, column 0, character 12973:
std.map.private.min-binding M2 X D,
std.map.private.remove-min-binding M2 Spilled1,
std.map.private.bal M1 X D Spilled1 R
std.map.private.merge M1 M2 R
File "builtin_map.elpi", line 90, column 0, character 13119:
!
std.map.private.remove std.map.private.empty _ _ std.map.private.empty
File "builtin_map.elpi", line 91, column 0, character 13148:
Cmp X V E,
std.map.private.remove.aux E Cmp L R V D X M
std.map.private.remove (std.map.private.node L V D R _) Cmp X M
File "builtin_map.elpi", line 92, column 0, character 13224:
std.map.private.merge L R M
std.map.private.remove.aux eq _ L R _ _ _ M
File "builtin_map.elpi", line 93, column 0, character 13270:
std.map.private.remove L Cmp X Spilled1,
std.map.private.bal Spilled1 V D R M
std.map.private.remove.aux lt Cmp L R V D X M
File "builtin_map.elpi", line 94, column 0, character 13333:
std.map.private.remove R Cmp X Spilled1,
std.map.private.bal L V D Spilled1 M
std.map.private.remove.aux gt Cmp L R V D X M
File "builtin_map.elpi", line 97, column 0, character 13460:
std.map.private.bindings std.map.private.empty X X
File "builtin_map.elpi", line 98, column 0, character 13480:
std.map.private.bindings R X Spilled1,
std.map.private.bindings L
[
pr V D | Spilled1
]
X1
std.map.private.bindings (std.map.private.node L V D R _) X X1
File "builtin_set.elpi", line 7, column 0, character 19405:
std.set.make Cmp (std.set std.set.private.empty Cmp)
File "builtin_set.elpi", line 11, column 0, character 19502:
std.set.private.mem M Cmp E
std.set.mem E (std.set M Cmp)
File "builtin_set.elpi", line 15, column 0, character 19617:
std.set.private.add M Cmp E M1
std.set.add E (std.set M Cmp) (std.set M1 Cmp)
File "builtin_set.elpi", line 19, column 0, character 19759:
std.set.private.remove M Cmp E M1
std.set.remove E (std.set M Cmp) (std.set M1 Cmp)
File "builtin_set.elpi", line 23, column 0, character 19916:
std.set.private.cardinal M N
std.set.cardinal (std.set M _) N
File "builtin_set.elpi", line 26, column 0, character 20004:
std.set.private.elements M [] L
std.set.elements (std.set M _) L
File "builtin_set.elpi", line 36, column 0, character 20224:
std.set.private.height std.set.private.empty 0
File "builtin_set.elpi", line 37, column 0, character 20240:
std.set.private.height (std.set.private.node _ _ _ H) H
File "builtin_set.elpi", line 40, column 0, character 20310:
std.set.private.height L Spilled1,
std.set.private.height R Spilled2,
std.max Spilled1 Spilled2 Spilled3,
H is 
Spilled3 + 
1
std.set.private.create L E R (std.set.private.node L E R H)
File "builtin_set.elpi", line 43, column 0, character 20425:
std.set.private.height L HL,
std.set.private.height R HR,
HL2 is 
HL + 
2,
HR2 is 
HR + 
2,
std.set.private.bal.aux HL HR HL2 HR2 L E R T
std.set.private.bal L E R T
File "builtin_set.elpi", line 50, column 0, character 20538:
> HL HR2,
std.set.private.height LL Spilled2,
std.set.private.height LR Spilled3,
>= Spilled2 Spilled3,
!,
std.set.private.create LR X R Spilled1,
std.set.private.create LL LV Spilled1 T
std.set.private.bal.aux HL _ _ HR2 (std.set.private.node LL LV LR _) X R T
File "builtin_set.elpi", line 53, column 0, character 20661:
> HL HR2,
!,
std.set.private.create LL LV LRL Spilled1,
std.set.private.create LRR X R Spilled2,
std.set.private.create Spilled1 LRV Spilled2 T
std.set.private.bal.aux HL _ _ HR2 (std.set.private.node LL LV (std.set.private.node LRL LRV LRR _) _) X R T
File "builtin_set.elpi", line 56, column 0, character 20792:
> HR HL2,
std.set.private.height RR Spilled2,
std.set.private.height RL Spilled3,
>= Spilled2 Spilled3,
!,
std.set.private.create L X RL Spilled1,
std.set.private.create Spilled1 RV RR T
std.set.private.bal.aux _ HR HL2 _ L X (std.set.private.node RL RV RR _) T
File "builtin_set.elpi", line 59, column 0, character 20915:
> HR HL2,
!,
std.set.private.create L X RLL Spilled1,
std.set.private.create RLR RV RR Spilled2,
std.set.private.create Spilled1 RLV Spilled2 T
std.set.private.bal.aux _ HR HL2 _ L X (std.set.private.node (std.set.private.node RLL RLV RLR _) RV RR _) T
File "builtin_set.elpi", line 62, column 0, character 21046:
std.set.private.create L E R T
std.set.private.bal.aux _ _ _ _ L E R T
File "builtin_set.elpi", line 65, column 0, character 21149:
std.set.private.create std.set.private.empty E std.set.private.empty T
std.set.private.add std.set.private.empty _ E T
File "builtin_set.elpi", line 66, column 0, character 21192:
Cmp X1 X E,
std.set.private.add.aux E Cmp L R X X1 H S
std.set.private.add (std.set.private.node L X R H) Cmp X1 S
File "builtin_set.elpi", line 67, column 0, character 21263:
std.set.private.add.aux eq _ L R X _ H (std.set.private.node L X R H)
File "builtin_set.elpi", line 68, column 0, character 21302:
std.set.private.add L Cmp X Spilled1,
std.set.private.bal Spilled1 E R T
std.set.private.add.aux lt Cmp L R E X _ T
File "builtin_set.elpi", line 69, column 0, character 21357:
std.set.private.add R Cmp X Spilled1,
std.set.private.bal L E Spilled1 T
std.set.private.add.aux gt Cmp L R E X _ T
File "builtin_set.elpi", line 72, column 0, character 21463:
Cmp E K O,
std.set.private.mem.aux O Cmp L R E
std.set.private.mem (std.set.private.node L K R _) Cmp E
File "builtin_set.elpi", line 73, column 0, character 21523:
std.set.private.mem.aux eq _ _ _ _
File "builtin_set.elpi", line 74, column 0, character 21543:
std.set.private.mem L Cmp E
std.set.private.mem.aux lt Cmp L _ E
File "builtin_set.elpi", line 75, column 0, character 21580:
std.set.private.mem R Cmp E
std.set.private.mem.aux gt Cmp _ R E
File "builtin_set.elpi", line 78, column 0, character 21660:
!
std.set.private.remove-min-binding (std.set.private.node std.set.private.empty _ R _) R
File "builtin_set.elpi", line 79, column 0, character 21706:
std.set.private.remove-min-binding L Spilled1,
std.set.private.bal Spilled1 E R X
std.set.private.remove-min-binding (std.set.private.node L E R _) X
File "builtin_set.elpi", line 82, column 0, character 21811:
!
std.set.private.min-binding (std.set.private.node std.set.private.empty E _ _) E
File "builtin_set.elpi", line 83, column 0, character 21850:
std.set.private.min-binding L E
std.set.private.min-binding (std.set.private.node L _ _ _) E
File "builtin_set.elpi", line 86, column 0, character 21938:
!
std.set.private.merge std.set.private.empty X X
File "builtin_set.elpi", line 87, column 0, character 21960:
!
std.set.private.merge X std.set.private.empty X
File "builtin_set.elpi", line 88, column 0, character 21982:
std.set.private.min-binding M2 X,
std.set.private.remove-min-binding M2 Spilled1,
std.set.private.bal M1 X Spilled1 R
std.set.private.merge M1 M2 R
File "builtin_set.elpi", line 93, column 0, character 22120:
std.set.private.remove std.set.private.empty _ _ std.set.private.empty
File "builtin_set.elpi", line 94, column 0, character 22144:
Cmp X E O,
std.set.private.remove.aux O Cmp L R E X M
std.set.private.remove (std.set.private.node L E R _) Cmp X M
File "builtin_set.elpi", line 95, column 0, character 22216:
std.set.private.merge L R M
std.set.private.remove.aux eq _ L R _ _ M
File "builtin_set.elpi", line 96, column 0, character 22260:
std.set.private.remove L Cmp X Spilled1,
std.set.private.bal Spilled1 E R M
std.set.private.remove.aux lt Cmp L R E X M
File "builtin_set.elpi", line 97, column 0, character 22319:
std.set.private.remove R Cmp X Spilled1,
std.set.private.bal L E Spilled1 M
std.set.private.remove.aux gt Cmp L R E X M
File "builtin_set.elpi", line 100, column 0, character 22409:
std.set.private.cardinal std.set.private.empty 0
File "builtin_set.elpi", line 101, column 0, character 22427:
std.set.private.cardinal L Spilled1,
std.set.private.cardinal R Spilled2,
N is 
Spilled1 + 
1 + 
Spilled2
std.set.private.cardinal (std.set.private.node L _ R _) N
File "builtin_set.elpi", line 104, column 0, character 22538:
std.set.private.elements std.set.private.empty X X
File "builtin_set.elpi", line 105, column 0, character 22558:
std.set.private.elements R Acc Spilled1,
std.set.private.elements L
[
E | Spilled1
]
X
std.set.private.elements (std.set.private.node L E R _) Acc X
File "builtin_set.elpi", line 255, column 0, character 27689:
term_to_string T T1,
output S T1
printterm S T
File "builtin_set.elpi", line 259, column 0, character 27757:
flush std_out,
input_line std_in X,
string_to_term X S
read S
File "(stdin)", line 7, column 3, character 142:
whd Hd (fun F),
!,
whd (F Arg) Reduct
whd (app Hd Arg) Reduct
File "(stdin)", line 11, column 3, character 265:
Reduct = 
X
whd X Reduct
File "(stdin)", line 10, column 3, character 294:
of Hd (arr A B),
of Arg A
of (app Hd Arg) B
File "(stdin)", line 15, column 3, character 459:
∀x1.
of x1 A ⇒ 
of (F x1) B
of (fun F) (arr A B)