mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
fix definition of Nat.pow
This commit is contained in:
parent
396d52319e
commit
c1b0f7bd0c
@ -1,10 +1,8 @@
|
||||
// x ^ y
|
||||
Nat.pow(x: Nat, y: Nat): Nat
|
||||
Nat.pow.aux(x, y, 1)
|
||||
|
||||
Nat.pow.aux(x: Nat, y: Nat, aux: Nat): Nat
|
||||
Nat.pow(x : Nat, y : Nat) : Nat
|
||||
case y {
|
||||
zero: x
|
||||
succ: Nat.pow.aux(x, y.pred, Nat.mul(aux, 2))
|
||||
zero:
|
||||
Nat.succ(Nat.zero)
|
||||
succ:
|
||||
Nat.mul(x, Nat.pow(x,y.pred))
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user