mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
8 lines
117 B
Python
8 lines
117 B
Python
|
|
||
|
|
def fact(n):
|
||
|
|
#@ ensures result >= 1
|
||
|
|
#@ variant n
|
||
|
|
if n <= 1:
|
||
|
|
return 1
|
||
|
|
return n * fact(n - 1)
|