darcsweb - verified/path_pure_proofs.glob

DIGEST d9c424371a23000e25fb2ff5a9170c9a
Fpath_pure_proofs
R85:89 Stdlib.Strings.Ascii <> <> lib
R91:96 Stdlib.Strings.String <> <> lib
R98:101 Stdlib.Bool.Bool <> <> lib
R103:106 Stdlib.Lists.List <> <> lib
R124:132 path_pure <> <> lib
R143:155 Stdlib.Lists.List ListNotations <> mod
prf 238:253 <> split_path_empty
R270:272 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R257:266 path_pure <> split_path def
R273:275 Corelib.Init.Datatypes <> nil constr
prf 310:326 <> split_path_single
R344:346 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R330:339 path_pure <> split_path def
R350:353 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R354:356 Corelib.Init.Datatypes <> nil constr
prf 403:419 <> split_path_simple
R439:441 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R423:432 path_pure <> split_path def
R445:448 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R452:455 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R456:458 Corelib.Init.Datatypes <> nil constr
prf 505:520 <> split_path_three
R548:550 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R524:533 path_pure <> split_path def
R556:559 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R566:569 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R574:577 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R578:580 Corelib.Init.Datatypes <> nil constr
prf 627:650 <> split_path_leading_slash
R671:673 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R654:663 path_pure <> split_path def
R676:679 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R685:688 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R689:691 Corelib.Init.Datatypes <> nil constr
prf 738:762 <> split_path_trailing_slash
R783:785 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R766:775 path_pure <> split_path def
R791:794 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R797:800 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R801:803 Corelib.Init.Datatypes <> nil constr
prf 911:928 <> safe_rejects_empty
R951:953 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R932:947 path_pure <> is_safe_sub_path def
R954:958 Corelib.Init.Datatypes <> false constr
prf 993:1011 <> safe_rejects_dotdot
R1036:1038 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1015:1030 path_pure <> is_safe_sub_path def
R1039:1043 Corelib.Init.Datatypes <> false constr
prf 1090:1105 <> safe_rejects_dot
R1129:1131 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1109:1124 path_pure <> is_safe_sub_path def
R1132:1136 Corelib.Init.Datatypes <> false constr
prf 1183:1200 <> safe_rejects_darcs
R1229:1231 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1204:1219 path_pure <> is_safe_sub_path def
R1232:1236 Corelib.Init.Datatypes <> false constr
prf 1283:1298 <> safe_rejects_git
R1325:1327 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1302:1317 path_pure <> is_safe_sub_path def
R1328:1332 Corelib.Init.Datatypes <> false constr
prf 1379:1397 <> safe_rejects_hidden
R1427:1429 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1401:1416 path_pure <> is_safe_sub_path def
R1430:1434 Corelib.Init.Datatypes <> false constr
prf 1481:1506 <> safe_rejects_nested_dotdot
R1539:1541 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1510:1525 path_pure <> is_safe_sub_path def
R1542:1546 Corelib.Init.Datatypes <> false constr
prf 1593:1617 <> safe_rejects_darcs_nested
R1657:1659 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1621:1636 path_pure <> is_safe_sub_path def
R1660:1664 Corelib.Init.Datatypes <> false constr
prf 1711:1736 <> safe_rejects_hidden_nested
R1775:1777 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1740:1755 path_pure <> is_safe_sub_path def
R1778:1782 Corelib.Init.Datatypes <> false constr
prf 1892:1910 <> safe_accepts_simple
R1936:1938 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1914:1929 path_pure <> is_safe_sub_path def
R1939:1942 Corelib.Init.Datatypes <> true constr
prf 1989:2007 <> safe_accepts_nested
R2041:2043 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2011:2026 path_pure <> is_safe_sub_path def
R2044:2047 Corelib.Init.Datatypes <> true constr
prf 2094:2110 <> safe_accepts_deep
R2153:2155 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2114:2129 path_pure <> is_safe_sub_path def
R2156:2159 Corelib.Init.Datatypes <> true constr
prf 2206:2228 <> safe_accepts_underscore
R2265:2267 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2232:2247 path_pure <> is_safe_sub_path def
R2268:2271 Corelib.Init.Datatypes <> true constr
prf 2351:2370 <> trailing_slash_empty
R2395:2397 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2374:2391 path_pure <> add_trailing_slash def
prf 2435:2456 <> trailing_slash_already
R2486:2488 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2460:2477 path_pure <> add_trailing_slash def
prf 2542:2560 <> trailing_slash_adds
R2589:2591 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2564:2581 path_pure <> add_trailing_slash def
prf 2645:2663 <> trailing_slash_root
R2689:2691 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2667:2684 path_pure <> add_trailing_slash def
prf 2741:2773 <> trailing_slash_idempotent_example
R2832:2836 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2779:2796 path_pure <> add_trailing_slash def
R2799:2816 path_pure <> add_trailing_slash def
R2837:2854 path_pure <> add_trailing_slash def