Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | The code compiles with only GHC nats | Tom Smeding | 2024-05-15 |
| | |||
* | Shape/index hygiene | Tom Smeding | 2024-05-13 |
| | |||
* | Try to make up for ToINat not being injectiveflesh-out-sized-lists | Mikolaj Konarski | 2024-04-23 |
| | |||
* | Add ToINat | Mikolaj Konarski | 2024-04-22 |
| | |||
* | Rename inductive naturals to INat | Tom Smeding | 2024-04-14 |