val pow (#t: Type) (k: comm_monoid t) (x: t) (n: nat) : t
let rec pow (#t:Type) (k:comm_monoid t) (x:t) (n:nat) : t =
  if n = 0 then one
  else mul x (pow k x (n - 1))
val pow (#t: Type) (k: comm_monoid t) (x: t) (n: nat) : t
let rec pow (#t: Type) (k: comm_monoid t) (x: t) (n: nat) : t =
if n = 0 then one else mul x (pow k x (n - 1))
Lib.Exponentiation.Definition.fsti.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Lib.Exponentiation.Definition.fsti
Lib.Exponentiation.Definition.comm_monoid Prims.nat Prims.op_Equality Prims.int Lib.Exponentiation.Definition.one Prims.bool Lib.Exponentiation.Definition.mul Lib.Exponentiation.Definition.pow Prims.op_Subtraction
module Lib.Exponentiation.Definition

open FStar.Mul

module Loops = Lib.LoopCombinators

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

//we don't require to have an inverse element to be an abelian group
//so this is just commutative monoid
inline_for_extraction
class comm_monoid (t:Type) = {
  one: t;
  mul: t -> t -> t;
  lemma_one: a:t -> Lemma (mul a one == a);
  lemma_mul_assoc: a:t -> b:t -> c:t -> Lemma (mul (mul a b) c == mul a (mul b c));
  lemma_mul_comm: a:t -> b:t -> Lemma (mul a b == mul b a)
  }


inline_for_extraction
class abelian_group (t:Type) = {
  cm:comm_monoid t;
  inverse: t -> t;
  lemma_inverse: a:t -> Lemma (mul (inverse a) a == one)
  }

let sqr (#t:Type) (k:comm_monoid t) (a:t) : t = mul a a


[@(strict_on_arguments [3])]
val pow (#t: Type) (k: comm_monoid t) (x: t) (n: nat) : t
k: Lib.Exponentiation.Definition.comm_monoid t -> x: t -> n: Prims.nat -> t