Sum.sign
Code: Alles auswählen
SIGNATURE Sum
IMPORT Nat ONLY nat
Seq ONLY seq
FUN sum : seq[nat] -> nat
Code: Alles auswählen
IMPLEMENTATION Sum
IMPORT Nat COMPLETELY
Seq COMPLETELY
SeqReduce COMPLETELY
DEF sum(ns) == (+, 0) \ ns