piercemaloney/coqgym_coq_projects_v1
收藏Hugging Face2024-02-29 更新2024-03-04 收录
下载链接：
https://hf-mirror.com/datasets/piercemaloney/coqgym_coq_projects_v1
下载链接
链接失效反馈官方服务：
资源简介：
---
dataset_info:
features:
- name: text
dtype: string
splits:
- name: finmap
num_bytes: 745110
num_examples: 3
- name: GeometricAlgebra
num_bytes: 2180457
num_examples: 8
- name: bdds
num_bytes: 11537326
num_examples: 15
- name: topology
num_bytes: 1998914
num_examples: 32
- name: euler_formula
num_bytes: 2157257
num_examples: 3
- name: ruler_compass_geometry
num_bytes: 105862
num_examples: 10
- name: twoSquare
num_bytes: 219009
num_examples: 2
- name: zfc
num_bytes: 605621
num_examples: 11
- name: shuffle
num_bytes: 87431
num_examples: 6
- name: three_gap
num_bytes: 315458
num_examples: 7
- name: regexp
num_bytes: 116907
num_examples: 7
- name: automata
num_bytes: 1075636
num_examples: 25
- name: izf
num_bytes: 146423
num_examples: 8
- name: railroad_crossing
num_bytes: 202543
num_examples: 1
- name: idxassoc
num_bytes: 139339
num_examples: 2
- name: hoare_tut
num_bytes: 39069
num_examples: 3
- name: lesniewski_mereology
num_bytes: 123636
num_examples: 2
- name: additions
num_bytes: 147048
num_examples: 20
- name: checker
num_bytes: 6689
num_examples: 2
- name: domain_theory
num_bytes: 67545
num_examples: 4
- name: propcalc
num_bytes: 54422
num_examples: 5
- name: area_method
num_bytes: 1578799
num_examples: 38
- name: ails
num_bytes: 521926
num_examples: 11
- name: dep_map
num_bytes: 24951
num_examples: 2
- name: markov
num_bytes: 102887
num_examples: 1
- name: rsa
num_bytes: 180155
num_examples: 5
- name: goedel
num_bytes: 9110441
num_examples: 44
- name: bigenough
num_bytes: 5031
num_examples: 1
- name: generic_environments
num_bytes: 142529
num_examples: 2
- name: ctltctl
num_bytes: 61038
num_examples: 3
- name: schroeder
num_bytes: 24958
num_examples: 4
- name: weak_up_to
num_bytes: 175365
num_examples: 10
- name: groups
num_bytes: 11115
num_examples: 1
- name: pocklington
num_bytes: 617483
num_examples: 13
- name: mini_compiler
num_bytes: 14459
num_examples: 1
- name: StructTact
num_bytes: 293887
num_examples: 17
- name: exceptions
num_bytes: 8962
num_examples: 1
- name: coqrel
num_bytes: 196290
num_examples: 12
- name: higman_s
num_bytes: 198793
num_examples: 5
- name: rem
num_bytes: 14504
num_examples: 1
- name: tree_automata
num_bytes: 1972575
num_examples: 17
- name: higman_cf
num_bytes: 49720
num_examples: 2
- name: coqoban
num_bytes: 38285
num_examples: 1
- name: search_trees
num_bytes: 59332
num_examples: 5
- name: ieee754
num_bytes: 35416
num_examples: 3
- name: jordan_curve_theorem
num_bytes: 12530912
num_examples: 10
- name: hedges
num_bytes: 360884
num_examples: 1
- name: zorns_lemma
num_bytes: 608752
num_examples: 19
- name: tortoise_hare_algorithm
num_bytes: 10084
num_examples: 1
- name: mod_red
num_bytes: 636981
num_examples: 5
- name: traversable_fincontainer
num_bytes: 429019
num_examples: 1
- name: buchberger
num_bytes: 2422607
num_examples: 29
- name: constructive_geometry
num_bytes: 80179
num_examples: 7
- name: tarski_geometry
num_bytes: 112419
num_examples: 8
- name: int_map
num_bytes: 817835
num_examples: 13
- name: float
num_bytes: 2994074
num_examples: 31
- name: InfSeqExt
num_bytes: 106656
num_examples: 5
- name: zchinese
num_bytes: 62626
num_examples: 6
- name: smc
num_bytes: 6045540
num_examples: 15
- name: pts
num_bytes: 72482
num_examples: 8
- name: param_pi
num_bytes: 2596347
num_examples: 11
- name: axiomatic_abp
num_bytes: 1204713
num_examples: 7
- name: lambda
num_bytes: 181085
num_examples: 10
- name: maths
num_bytes: 37685
num_examples: 3
- name: quicksort_complexity
num_bytes: 489164
num_examples: 28
- name: fssec_model
num_bytes: 1569135
num_examples: 25
- name: ipc
num_bytes: 3108901
num_examples: 31
- name: chinese
num_bytes: 208365
num_examples: 13
- name: cours_de_coq
num_bytes: 71295
num_examples: 11
- name: graphs
num_bytes: 644609
num_examples: 2
- name: dictionaries
num_bytes: 67746
num_examples: 1
- name: free_groups
num_bytes: 63973
num_examples: 1
- name: ramsey
num_bytes: 11734
num_examples: 1
- name: angles
num_bytes: 322579
num_examples: 5
- name: orb_stab
num_bytes: 204783
num_examples: 1
- name: qarith_stern_brocot
num_bytes: 10873352
num_examples: 35
- name: group_theory
num_bytes: 65160
num_examples: 5
- name: demos
num_bytes: 62208
num_examples: 5
- name: distributed_reference_counting
num_bytes: 20874
num_examples: 1
- name: subst
num_bytes: 362195
num_examples: 17
- name: miniml
num_bytes: 114099
num_examples: 1
- name: algebra
num_bytes: 3275753
num_examples: 65
- name: fermat4
num_bytes: 172156
num_examples: 5
- name: otway_rees
num_bytes: 226052
num_examples: 19
- name: PolTac
num_bytes: 157370
num_examples: 13
- name: fundamental_arithmetics
num_bytes: 308733
num_examples: 8
download_size: 11353498
dataset_size: 91221719
configs:
- config_name: default
data_files:
- split: finmap
path: data/finmap-*
- split: GeometricAlgebra
path: data/GeometricAlgebra-*
- split: bdds
path: data/bdds-*
- split: topology
path: data/topology-*
- split: euler_formula
path: data/euler_formula-*
- split: ruler_compass_geometry
path: data/ruler_compass_geometry-*
- split: twoSquare
path: data/twoSquare-*
- split: zfc
path: data/zfc-*
- split: shuffle
path: data/shuffle-*
- split: three_gap
path: data/three_gap-*
- split: regexp
path: data/regexp-*
- split: automata
path: data/automata-*
- split: izf
path: data/izf-*
- split: railroad_crossing
path: data/railroad_crossing-*
- split: idxassoc
path: data/idxassoc-*
- split: hoare_tut
path: data/hoare_tut-*
- split: lesniewski_mereology
path: data/lesniewski_mereology-*
- split: additions
path: data/additions-*
- split: checker
path: data/checker-*
- split: domain_theory
path: data/domain_theory-*
- split: propcalc
path: data/propcalc-*
- split: area_method
path: data/area_method-*
- split: ails
path: data/ails-*
- split: dep_map
path: data/dep_map-*
- split: markov
path: data/markov-*
- split: rsa
path: data/rsa-*
- split: goedel
path: data/goedel-*
- split: bigenough
path: data/bigenough-*
- split: generic_environments
path: data/generic_environments-*
- split: ctltctl
path: data/ctltctl-*
- split: schroeder
path: data/schroeder-*
- split: weak_up_to
path: data/weak_up_to-*
- split: groups
path: data/groups-*
- split: pocklington
path: data/pocklington-*
- split: mini_compiler
path: data/mini_compiler-*
- split: StructTact
path: data/StructTact-*
- split: exceptions
path: data/exceptions-*
- split: coqrel
path: data/coqrel-*
- split: higman_s
path: data/higman_s-*
- split: rem
path: data/rem-*
- split: tree_automata
path: data/tree_automata-*
- split: higman_cf
path: data/higman_cf-*
- split: coqoban
path: data/coqoban-*
- split: search_trees
path: data/search_trees-*
- split: ieee754
path: data/ieee754-*
- split: jordan_curve_theorem
path: data/jordan_curve_theorem-*
- split: hedges
path: data/hedges-*
- split: zorns_lemma
path: data/zorns_lemma-*
- split: tortoise_hare_algorithm
path: data/tortoise_hare_algorithm-*
- split: mod_red
path: data/mod_red-*
- split: traversable_fincontainer
path: data/traversable_fincontainer-*
- split: buchberger
path: data/buchberger-*
- split: constructive_geometry
path: data/constructive_geometry-*
- split: tarski_geometry
path: data/tarski_geometry-*
- split: int_map
path: data/int_map-*
- split: float
path: data/float-*
- split: InfSeqExt
path: data/InfSeqExt-*
- split: zchinese
path: data/zchinese-*
- split: smc
path: data/smc-*
- split: pts
path: data/pts-*
- split: param_pi
path: data/param_pi-*
- split: axiomatic_abp
path: data/axiomatic_abp-*
- split: lambda
path: data/lambda-*
- split: maths
path: data/maths-*
- split: quicksort_complexity
path: data/quicksort_complexity-*
- split: fssec_model
path: data/fssec_model-*
- split: ipc
path: data/ipc-*
- split: chinese
path: data/chinese-*
- split: cours_de_coq
path: data/cours_de_coq-*
- split: graphs
path: data/graphs-*
- split: dictionaries
path: data/dictionaries-*
- split: free_groups
path: data/free_groups-*
- split: ramsey
path: data/ramsey-*
- split: angles
path: data/angles-*
- split: orb_stab
path: data/orb_stab-*
- split: qarith_stern_brocot
path: data/qarith_stern_brocot-*
- split: group_theory
path: data/group_theory-*
- split: demos
path: data/demos-*
- split: distributed_reference_counting
path: data/distributed_reference_counting-*
- split: subst
path: data/subst-*
- split: miniml
path: data/miniml-*
- split: algebra
path: data/algebra-*
- split: fermat4
path: data/fermat4-*
- split: otway_rees
path: data/otway_rees-*
- split: PolTac
path: data/PolTac-*
- split: fundamental_arithmetics
path: data/fundamental_arithmetics-*
---
提供机构：
piercemaloney
原始信息汇总
数据集概述
数据集特征
- 特征名称: text
- 数据类型: string
数据集分割
- finmap
- 字节数: 745110
- 样本数: 3
- GeometricAlgebra
- 字节数: 2180457
- 样本数: 8
- bdds
- 字节数: 11537326
- 样本数: 15
- topology
- 字节数: 1998914
- 样本数: 32
- euler_formula
- 字节数: 2157257
- 样本数: 3
- ruler_compass_geometry
- 字节数: 105862
- 样本数: 10
- twoSquare
- 字节数: 219009
- 样本数: 2
- zfc
- 字节数: 605621
- 样本数: 11
- shuffle
- 字节数: 87431
- 样本数: 6
- three_gap
- 字节数: 315458
- 样本数: 7
- regexp
- 字节数: 116907
- 样本数: 7
- automata
- 字节数: 1075636
- 样本数: 25
- izf
- 字节数: 146423
- 样本数: 8
- railroad_crossing
- 字节数: 202543
- 样本数: 1
- idxassoc
- 字节数: 139339
- 样本数: 2
- hoare_tut
- 字节数: 39069
- 样本数: 3
- lesniewski_mereology
- 字节数: 123636
- 样本数: 2
- additions
- 字节数: 147048
- 样本数: 20
- checker
- 字节数: 6689
- 样本数: 2
- domain_theory
- 字节数: 67545
- 样本数: 4
- propcalc
- 字节数: 54422
- 样本数: 5
- area_method
- 字节数: 1578799
- 样本数: 38
- ails
- 字节数: 521926
- 样本数: 11
- dep_map
- 字节数: 24951
- 样本数: 2
- markov
- 字节数: 102887
- 样本数: 1
- rsa
- 字节数: 180155
- 样本数: 5
- goedel
- 字节数: 9110441
- 样本数: 44
- bigenough
- 字节数: 5031
- 样本数: 1
- generic_environments
- 字节数: 142529
- 样本数: 2
- ctltctl
- 字节数: 61038
- 样本数: 3
- schroeder
- 字节数: 24958
- 样本数: 4
- weak_up_to
- 字节数: 175365
- 样本数: 10
- groups
- 字节数: 11115
- 样本数: 1
- pocklington
- 字节数: 617483
- 样本数: 13
- mini_compiler
- 字节数: 14459
- 样本数: 1
- StructTact
- 字节数: 293887
- 样本数: 17
- exceptions
- 字节数: 8962
- 样本数: 1
- coqrel
- 字节数: 196290
- 样本数: 12
- higman_s
- 字节数: 198793
- 样本数: 5
- rem
- 字节数: 14504
- 样本数: 1
- tree_automata
- 字节数: 1972575
- 样本数: 17
- higman_cf
- 字节数: 49720
- 样本数: 2
- coqoban
- 字节数: 38285
- 样本数: 1
- search_trees
- 字节数: 59332
- 样本数: 5
- ieee754
- 字节数: 35416
- 样本数: 3
- jordan_curve_theorem
- 字节数: 12530912
- 样本数: 10
- hedges
- 字节数: 360884
- 样本数: 1
- zorns_lemma
- 字节数: 608752
- 样本数: 19
- tortoise_hare_algorithm
- 字节数: 10084
- 样本数: 1
- mod_red
- 字节数: 636981
- 样本数: 5
- traversable_fincontainer
- 字节数: 429019
- 样本数: 1
- buchberger
- 字节数: 2422607
- 样本数: 29
- constructive_geometry
- 字节数: 80179
- 样本数: 7
- tarski_geometry
- 字节数: 112419
- 样本数: 8
- int_map
- 字节数: 817835
- 样本数: 13
- float
- 字节数: 2994074
- 样本数: 31
- InfSeqExt
- 字节数: 106656
- 样本数: 5
- zchinese
- 字节数: 62626
- 样本数: 6
- smc
- 字节数: 6045540
- 样本数: 15
- pts
- 字节数: 72482
- 样本数: 8
- param_pi
- 字节数: 2596347
- 样本数: 11
- axiomatic_abp
- 字节数: 1204713
- 样本数: 7
- lambda
- 字节数: 181085
- 样本数: 10
- maths
- 字节数: 37685
- 样本数: 3
- quicksort_complexity
- 字节数: 489164
- 样本数: 28
- fssec_model
- 字节数: 1569135
- 样本数: 25
- ipc
- 字节数: 3108901
- 样本数: 31
- chinese
- 字节数: 208365
- 样本数: 13
- cours_de_coq
- 字节数: 71295
- 样本数: 11
- graphs
- 字节数: 644609
- 样本数: 2
- dictionaries
- 字节数: 67746
- 样本数: 1
- free_groups
- 字节数: 63973
- 样本数: 1
- ramsey
- 字节数: 11734
- 样本数: 1
- angles
- 字节数: 322579
- 样本数: 5
- orb_stab
- 字节数: 204783
- 样本数: 1
- qarith_stern_brocot
- 字节数: 10873352
- 样本数: 35
- group_theory
- 字节数: 65160
- 样本数: 5
- demos
- 字节数: 62208
- 样本数: 5
- distributed_reference_counting
- 字节数: 20874
- 样本数: 1
- subst
- 字节数: 362195
- 样本数: 17
- miniml
- 字节数: 114099
- 样本数: 1
- algebra
- 字节数: 3275753
- 样本数: 65
- fermat4
- 字节数: 172156
- 样本数: 5
- otway_rees
- 字节数: 226052
- 样本数: 19
- PolTac
- 字节数: 157370
- 样本数: 13
- fundamental_arithmetics
- 字节数: 308733
- 样本数: 8
数据集大小
- 下载大小: 11353498 字节
- 数据集大小: 91221719 字节
