aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorVincent Semeria2019-08-06 18:47:57 +0200
committerVincent Semeria2019-08-06 18:47:57 +0200
commiteab34b814f1d06767fee07690e3ab6a56236ccde (patch)
tree17c35936543da755bb89387b33b2465c62faa82c /kernel/type_errors.ml
parent76a11fb070cc2cf3c1ebce32cd692fa64c31767f (diff)
Prove the completeness of real numbers from logical axiom sig_not_dec
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions