docs: add comments

Anoma/Identity/Signing/Types.juvix

@@ -7,25 +7,44 @@ import Anoma.Identity.External open;
 axiom Signature : Type;
 
 axiom verify : {Message : Type}
-  -> (signature : Signature)
-  -> (message : Message)
-  -> (external : ExternalIdentity)
+  -- | The signature to verify.
+  -> Signature
+  -- | The message to verify against.
+  -> Message
+  -- | The signer external identity to verify against.
+  -> ExternalIdentity
+  -- | The verification result.
   -> Bool;
 
-axiom sign : {Message : Type} -> (message : Message) -> (internal : InternalIdentity) -> Signature;
+axiom sign : {Message : Type}
+  -- | The message to sign.
+  -> Message
+  -- | The signing internal identity .
+  -> InternalIdentity
+  -- | The resulting signature
+  -> Signature;
 
 module NonDetached;
   axiom SignedMessage : Type;
 
-  axiom verify : (signedMessage : SignedMessage) -> (external : ExternalIdentity) -> Bool;
+  verify (signedMessage : SignedMessage) (externalIdentity : ExternalIdentity) : Bool :=
+    case verifyWithMessage {Unit} signedMessage externalIdentity of
+      | just _ := true
+      | nothing := false;
 
   axiom verifyWithMessage : {Message : Type}
-    -> (signedMessage : SignedMessage)
-    -> (external : ExternalIdentity)
+    -- | The signed message to verify.
+    -> SignedMessage
+    -- | The signer external identity to verify against.
+    -> ExternalIdentity
+    -- | The original message.
     -> Maybe Message;
 
   axiom sign : {Message : Type}
-    -> (message : Message)
-    -> (internal : InternalIdentity)
+    -- | The message to sign.
+    -> Message
+    -- | The signing internal identity.
+    -> InternalIdentity
+    -- | The resulting signed message.
     -> SignedMessage;
 end;