From 2e606b03c8dbc594610e62ac260145ac26ebc699 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Oct 2008 12:58:35 -0400 Subject: Fix nasty de Bruijn substitution bug; TcSum demo --- demo/tcSum.ur | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 demo/tcSum.ur (limited to 'demo/tcSum.ur') diff --git a/demo/tcSum.ur b/demo/tcSum.ur new file mode 100644 index 00000000..53679116 --- /dev/null +++ b/demo/tcSum.ur @@ -0,0 +1,9 @@ +fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) = + foldUR [t] [fn _ => t] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc) + zero [fs] x + +fun main () = return + {[sum {A = 0, B = 1}]}
+ {[sum {C = 2.1, D = 3.2, E = 4.3}]} + -- cgit v1.2.3