projects / cubicaltt.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35fc628) | patch
eval ignores opaqueness
authorRafaël Bocquet <rafael.bocquet@ens.fr>
Wed, 13 Apr 2016 08:48:59 +0000 (10:48 +0200)
committerRafaël Bocquet <rafael.bocquet@ens.fr>
Wed, 13 Apr 2016 08:48:59 +0000 (10:48 +0200)
commit8c970660b55c443a0f1c3ceb40b0ca76bf1f6910
tree60f19dbcc69cc67c346c41ead861ad8f10a59bcctree | snapshot
parent35fc628baccd8f4a7fd39ba609b67a3cd0e88e0ecommit | diff
eval ignores opaqueness
Proof of BZ = (X : (A:U) * (A->A)) * inh (X = (Z, sucZ))
CTT.hs diff | blob | blame | history
Eval.hs diff | blob | blame | history
examples/torsor.ctt diff | blob | blame | history
My fork of cubicaltt with web interface using Reflex.