|
|
|
|
|
|
by zozbot234
57 days ago
|
|
|
There is indeed no difference if your dependent-typing approach is using reflection (where the checked term is actually a program that's logically proven to result in a a correct proof when executed - such as, commonly, by running a decision procedure) but that's not a common approach. |
|
|