diff --git a/theories/list.why b/theories/list.why index ea6ab78d0869163e9e5c4cb9af769efbc8549037..8b2271cee57eea6f4fe0850542e1cffb5432806a 100644 --- a/theories/list.why +++ b/theories/list.why @@ -486,6 +486,18 @@ theory Prefix end +theory Sum + + use export List + use import int.Int + + function sum (l: list int) : int = match l with + | Nil -> 0 + | Cons x r -> x + sum r + end + +end + (** {2 Induction on lists} *) theory Induction