@@ -36,10 +36,11 @@ Module Primitives.
36
36
World ->
37
37
TokenQuantity token_kind.
38
38
39
+ (** Get the number of token that a [spender] is allowed to spend from a [user] *)
39
40
Parameter get_allowance :
40
41
forall (token_kind : TokenKind),
41
- User -> (* user *)
42
- User -> (* spender *)
42
+ forall ( user : User),
43
+ forall ( spender : User),
43
44
World ->
44
45
TokenQuantity token_kind.
45
46
@@ -53,10 +54,11 @@ Module Primitives.
53
54
World ->
54
55
option World.
55
56
57
+ (** Set the allowance for a certain [spender] at a certain amount from the account of a [user] *)
56
58
Parameter approve :
57
59
forall (token_kind : TokenKind),
58
- User -> (* user *)
59
- User -> (* spender *)
60
+ forall ( user : User),
61
+ forall ( spender : User),
60
62
TokenQuantity token_kind ->
61
63
World ->
62
64
World.
@@ -274,7 +276,7 @@ Module Erc20.
274
276
(* We run the action to get the balance *)
275
277
let ! balance := M.MakeAction (Action.GetBalance token_kind user) in
276
278
M.Pure (Some (balance, state))
277
- (* "getAllowance" *)
279
+ (* The "allowance" entrypoint *)
278
280
| Command.GetAllowance user spender =>
279
281
let ! allowance := M.MakeAction (Action.GetAllowance token_kind user spender) in
280
282
M.Pure (Some (allowance, state))
@@ -286,6 +288,7 @@ Module Erc20.
286
288
M.Pure (Some (tt, state))
287
289
else
288
290
M.Pure None
291
+ (* The "approve" entrypoint *)
289
292
| Command.Approve spender value =>
290
293
let ! _ := M.MakeAction (Action.Approve token_kind sender spender value) in
291
294
M.Pure (Some (tt, state))
0 commit comments