Network.URL.General

通用 URL 处理模块
提供基本的 URL 解析和字符串化功能

Definitions

data GeneralURL : Type

  表示一个通用的 URL 结构
  @scheme URL 的协议部分
  @specific URL 的具体内容部分

Totality: total
Visibility: public export
Constructor: 

MkGeneralURL : String -> String -> GeneralURL

Hints:

Eq GeneralURL

Show GeneralURL

parse : String -> Maybe GeneralURL

  将字符串解析为 URL
  @str 要解析的字符串
  @returns 如果解析成功则返回 Just GeneralURL，否则返回 Nothing

Visibility: public export

stringify : GeneralURL -> String

  将 URL 转换为字符串形式
  @url 要转换的 URL
  @returns URL 的字符串表示

Visibility: public export