diff lib/basis.urs @ 417:e0e9e9eca1cb

Fix nasty de Bruijn substitution bug; TcSum demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 12:58:35 -0400
parents c5a3d223f157
children 0ce90d4d9ae7
line wrap: on
line diff
--- a/lib/basis.urs	Thu Oct 23 11:59:48 2008 -0400
+++ b/lib/basis.urs	Thu Oct 23 12:58:35 2008 -0400
@@ -20,6 +20,7 @@
 val eq_bool : eq bool
 
 class num
+val zero : t ::: Type -> num t -> t
 val neg : t ::: Type -> num t -> t -> t
 val plus : t ::: Type -> num t -> t -> t -> t
 val minus : t ::: Type -> num t -> t -> t -> t