aya-dev icon indicating copy to clipboard operation
aya-dev copied to clipboard

Published 20 hours ago • verified publisher icon aya-prover

Cubical subtypes

Open ice1000 opened this issue 3 years ago • 1 comments

This is a task.

ice1000 avatar Sep 22 '22 02:09 ice1000

Add PrimTerms inSub, outSub, Sub and implement typechecking and computation rules

lunalunaa avatar Sep 25 '22 20:09 lunalunaa

Closing for now, because the rules are implemented. Coercions are yet to be done.

ice1000 avatar Dec 17 '22 03:12 ice1000