RedPRL
受 Nuprl 启发而开发的基于策略的计算笛卡尔立方类型理论证明助手。RedPRL 实现了两级立方类型理论，其中包括单等式宇宙、一些高级归纳类型和带有等式反射的严格等式类型。「A tactic-based proof assistant for computational Cartesian cubical type theory inspired by Nuprl. RedPRL implements a two-level cubical type theory which includes univalent universes, some higher inductive types, and strict equality types with equality reflection.」
Main metrics
Overview
| Name With Owner | RedPRL/sml-redprl |
|---|---|
| Primary Language | Standard ML |
| Program language | Standard ML (Language Count: 5) |
| Platform | |
| License: | MIT License |
| Release Count | 2 |
| Last Release Name | arxiv2017 (Posted on ) |
| First Release Name | v0.1.0 (Posted on ) |
| Created At | 2016-01-05 05:08:26 |
| Pushed At | 2023-01-01 19:34:01 |
| Last Commit At | 2019-11-04 16:09:24 |
| Stargazers Count | 228 |
| Watchers Count | 29 |
| Fork Count | 18 |
| Commits Count | 1013 |
| Has Issues Enabled | |
| Issues Count | 309 |
| Issue Open Count | 7 |
| Pull Requests Count | 369 |
| Pull Requests Open Count | 0 |
| Pull Requests Close Count | 21 |
| Has Wiki Enabled | |
| Is Archived | |
| Is Fork | |
| Is Locked | |
| Is Mirror | |
| Is Private |
