binghe
{
"type": "http://schema.org/Person",
"name": "",
"description": "",
"followers": "",
"url": "",
"location": "",
"languages": [
"Common Lisp",
"Common Lisp",
"C",
"Common Lisp",
"Standard ML",
"PostScript"
],
"users": [
{
"name": "@binghe",
"avatar": "https://avatars.githubusercontent.com/u/163421?s=64&v=4"
},
{
"name": "@binghe",
"avatar": "https://avatars.githubusercontent.com/u/163421?s=64&v=4"
},
{
"name": "View binghe's full-sized avatar",
"avatar": "https://avatars.githubusercontent.com/u/163421?v=4"
}
],
"topics": []
}
{
"avatar": "https://avatars.githubusercontent.com/u/163421?v=4",
"name": "Chun Tian",
"username": "binghe",
"description": "Common Lisp programmer, HOL proof engineer",
"location": "",
"vcard": "<!-- Generator: Adobe Illustrator 19.1.0, SVG Export Plug-In . SVG Version: 6.00 Build 0) --><svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" version=\"1.1\" id=\"Layer_1\" x=\"0px\" y=\"0px\" viewBox=\"0 0 256 256\" style=\"enable-background:new 0 0 256 256;\" xml:space=\"preserve\" aria-hidden=\"true\" class=\"octicon\" width=\"16\" height=\"16\">\n<path fill=\"currentColor\" fill-rule=\"evenodd\" d=\"M256,128c0,70.7-57.3,128-128,128C57.3,256,0,198.7,0,128C0,57.3,57.3,0,128,0C198.7,0,256,57.3,256,128z M86.3,186.2H70.9V79.1h15.4v48.4V186.2z M108.9,79.1h41.6c39.6,0,57,28.3,57,53.6c0,27.5-21.5,53.6-56.8,53.6h-41.8V79.1z M124.3,172.4h24.5 c34.9,0,42.9-26.5,42.9-39.7c0-21.5-13.7-39.7-43.7-39.7h-23.7V172.4z M88.7,56.8c0,5.5-4.5,10.1-10.1,10.1c-5.6,0-10.1-4.6-10.1-10.1c0-5.6,4.5-10.1,10.1-10.1 C84.2,46.7,88.7,51.3,88.7,56.8z\"></path>\n</svg>\n <a rel=\"nofollow me\" class=\"Link--primary wb-break-all\" href=\"https://orcid.org/0000-0002-2777-9443\">https://orcid.org/0000-0002-2777-9443</a>\n",
"vcardDetails": [
{
"name": "https://orcid.org/0000-0002-2777-9443",
"url": "https://orcid.org/0000-0002-2777-9443"
},
{
"name": "binghe.lisp",
"url": "https://www.facebook.com/binghe.lisp"
}
],
"orgs": [
{
"name": "@HOL-Theorem-Prover",
"avatar": "https://avatars.githubusercontent.com/u/8379840?s=64&v=4"
},
{
"name": "@usocket",
"avatar": "https://avatars.githubusercontent.com/u/8856374?s=64&v=4"
}
],
"sponsors": [],
"pinned": [
{
"name": "usocket/usocket",
"description": "Universal socket library for Common Lisp",
"language": ""
},
{
"name": "cl-net-snmp",
"description": "Simple Network Management Protocol (SNMP) for Common Lisp",
"language": ""
},
{
"name": "Acrobat-Actions",
"description": "Actions, Commands and Plug-ins for Adobe® Acrobat® Pro",
"language": ""
},
{
"name": "fm-plugin-tools",
"description": "A toolkit for FileMaker plug-in developments in Common Lisp",
"language": ""
},
{
"name": "HOL",
"description": "Forked sources of HOL4 (no cv_compute, etc.)",
"language": ""
},
{
"name": "axiom-code",
"description": "Axiom is a free, open source computer algebra system",
"language": ""
}
],
"pinnedHtml": [
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"24323422\" href=\"/usocket/usocket\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"owner text-normal\">usocket/</span><span class=\"repo\">usocket</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-bd3fef91-e145-4ae3-81c2-4db0359ba96b\" for=\"24323422\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">usocket/usocket</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n Universal socket library for Common Lisp\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #3fb68b\"></span>\n <span itemprop=\"programmingLanguage\">Common Lisp</span>\n</span>\n\n <a href=\"/usocket/usocket/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 243\n </a>\n <a href=\"/usocket/usocket/forks\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"forks\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo-forked\">\n <path d=\"M5 5.372v.878c0 .414.336.75.75.75h4.5a.75.75 0 0 0 .75-.75v-.878a2.25 2.25 0 1 1 1.5 0v.878a2.25 2.25 0 0 1-2.25 2.25h-1.5v2.128a2.251 2.251 0 1 1-1.5 0V8.5h-1.5A2.25 2.25 0 0 1 3.5 6.25v-.878a2.25 2.25 0 1 1 1.5 0ZM5 3.25a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Zm6.75.75a.75.75 0 1 0 0-1.5.75.75 0 0 0 0 1.5Zm-3 8.75a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Z\"></path>\n</svg>\n 54\n </a>\n </p>\n ",
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"101759003\" href=\"/binghe/cl-net-snmp\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"repo\">cl-net-snmp</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-f13f7f73-21b9-4ebd-b03d-06db6491880a\" for=\"101759003\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">cl-net-snmp</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n Simple Network Management Protocol (SNMP) for Common Lisp\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #3fb68b\"></span>\n <span itemprop=\"programmingLanguage\">Common Lisp</span>\n</span>\n\n <a href=\"/binghe/cl-net-snmp/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 25\n </a>\n <a href=\"/binghe/cl-net-snmp/forks\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"forks\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo-forked\">\n <path d=\"M5 5.372v.878c0 .414.336.75.75.75h4.5a.75.75 0 0 0 .75-.75v-.878a2.25 2.25 0 1 1 1.5 0v.878a2.25 2.25 0 0 1-2.25 2.25h-1.5v2.128a2.251 2.251 0 1 1-1.5 0V8.5h-1.5A2.25 2.25 0 0 1 3.5 6.25v-.878a2.25 2.25 0 1 1 1.5 0ZM5 3.25a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Zm6.75.75a.75.75 0 1 0 0-1.5.75.75 0 0 0 0 1.5Zm-3 8.75a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Z\"></path>\n</svg>\n 2\n </a>\n </p>\n ",
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"160654171\" href=\"/binghe/Acrobat-Actions\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"repo\">Acrobat-Actions</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-9a119144-ff98-4ebc-8a24-09440a50ca98\" for=\"160654171\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">Acrobat-Actions</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n Actions, Commands and Plug-ins for Adobe® Acrobat® Pro\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #555555\"></span>\n <span itemprop=\"programmingLanguage\">C</span>\n</span>\n\n <a href=\"/binghe/Acrobat-Actions/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 78\n </a>\n <a href=\"/binghe/Acrobat-Actions/forks\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"forks\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo-forked\">\n <path d=\"M5 5.372v.878c0 .414.336.75.75.75h4.5a.75.75 0 0 0 .75-.75v-.878a2.25 2.25 0 1 1 1.5 0v.878a2.25 2.25 0 0 1-2.25 2.25h-1.5v2.128a2.251 2.251 0 1 1-1.5 0V8.5h-1.5A2.25 2.25 0 0 1 3.5 6.25v-.878a2.25 2.25 0 1 1 1.5 0ZM5 3.25a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Zm6.75.75a.75.75 0 1 0 0-1.5.75.75 0 0 0 0 1.5Zm-3 8.75a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Z\"></path>\n</svg>\n 21\n </a>\n </p>\n ",
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"141706645\" href=\"/binghe/fm-plugin-tools\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"repo\">fm-plugin-tools</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-6a6e82f5-21e1-45c2-936d-8de8625d060f\" for=\"141706645\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">fm-plugin-tools</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n A toolkit for FileMaker plug-in developments in Common Lisp\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #3fb68b\"></span>\n <span itemprop=\"programmingLanguage\">Common Lisp</span>\n</span>\n\n <a href=\"/binghe/fm-plugin-tools/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 14\n </a>\n <a href=\"/binghe/fm-plugin-tools/forks\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"forks\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo-forked\">\n <path d=\"M5 5.372v.878c0 .414.336.75.75.75h4.5a.75.75 0 0 0 .75-.75v-.878a2.25 2.25 0 1 1 1.5 0v.878a2.25 2.25 0 0 1-2.25 2.25h-1.5v2.128a2.251 2.251 0 1 1-1.5 0V8.5h-1.5A2.25 2.25 0 0 1 3.5 6.25v-.878a2.25 2.25 0 1 1 1.5 0ZM5 3.25a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Zm6.75.75a.75.75 0 1 0 0-1.5.75.75 0 0 0 0 1.5Zm-3 8.75a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Z\"></path>\n</svg>\n 4\n </a>\n </p>\n ",
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"74522925\" href=\"/binghe/HOL\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"repo\">HOL</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-c33603ab-ccae-488e-9b07-28dbec75ae47\" for=\"74522925\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">HOL</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n <p class=\"color-fg-muted text-small mt-2 mb-0\">\n Forked from <a class=\"Link--muted Link--inTextBlock\" href=\"/HOL-Theorem-Prover/HOL\">HOL-Theorem-Prover/HOL</a>\n </p>\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n Forked sources of HOL4 (no cv_compute, etc.)\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #dc566d\"></span>\n <span itemprop=\"programmingLanguage\">Standard ML</span>\n</span>\n\n <a href=\"/binghe/HOL/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 7\n </a>\n <a href=\"/binghe/HOL/forks\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"forks\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo-forked\">\n <path d=\"M5 5.372v.878c0 .414.336.75.75.75h4.5a.75.75 0 0 0 .75-.75v-.878a2.25 2.25 0 1 1 1.5 0v.878a2.25 2.25 0 0 1-2.25 2.25h-1.5v2.128a2.251 2.251 0 1 1-1.5 0V8.5h-1.5A2.25 2.25 0 0 1 3.5 6.25v-.878a2.25 2.25 0 1 1 1.5 0ZM5 3.25a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Zm6.75.75a.75.75 0 1 0 0-1.5.75.75 0 0 0 0 1.5Zm-3 8.75a.75.75 0 1 0-1.5 0 .75.75 0 0 0 1.5 0Z\"></path>\n</svg>\n 2\n </a>\n </p>\n ",
"\n <div class=\"d-flex width-full position-relative\">\n <div class=\"flex-1\">\n <svg aria-hidden=\"true\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-repo mr-1 tmp-mr-1 color-fg-muted\">\n <path d=\"M2 2.5A2.5 2.5 0 0 1 4.5 0h8.75a.75.75 0 0 1 .75.75v12.5a.75.75 0 0 1-.75.75h-2.5a.75.75 0 0 1 0-1.5h1.75v-2h-8a1 1 0 0 0-.714 1.7.75.75 0 1 1-1.072 1.05A2.495 2.495 0 0 1 2 11.5Zm10.5-1h-8a1 1 0 0 0-1 1v6.708A2.486 2.486 0 0 1 4.5 9h8ZM5 12.25a.25.25 0 0 1 .25-.25h3.5a.25.25 0 0 1 .25.25v3.25a.25.25 0 0 1-.4.2l-1.45-1.087a.249.249 0 0 0-.3 0L5.4 15.7a.25.25 0 0 1-.4-.2Z\"></path>\n</svg>\n <span data-view-component=\"true\" class=\"position-relative\"><a data-hydro-click=\"{"event_type":"user_profile.click","payload":{"profile_user_id":163421,"target":"PINNED_REPO","user_id":null,"originating_url":"https://github.com/binghe"}}\" data-hydro-click-hmac=\"4c664c85a15aa0a017c657580b53d9a614f026d0ec32a76f3a0e49a18a15aaff\" id=\"504095918\" href=\"/binghe/axiom-code\" data-view-component=\"true\" class=\"Link mr-1 tmp-mr-1 text-bold wb-break-word\"><span class=\"repo\">axiom-code</span></a> <tool-tip data-direction=\"n\" id=\"tooltip-90c1b3b9-1b69-48af-a4ff-5bf9b75406c5\" for=\"504095918\" popover=\"manual\" data-type=\"label\" data-view-component=\"true\" class=\"sr-only position-absolute\">axiom-code</tool-tip></span> <span></span><span class=\"Label Label--secondary v-align-middle mt-1 no-wrap v-align-baseline Label--inline\">Public</span>\n </div>\n </div>\n\n <p class=\"color-fg-muted text-small mt-2 mb-0\">\n Forked from <a class=\"Link--muted Link--inTextBlock\" href=\"/daly/axiom\">daly/axiom</a>\n </p>\n\n <p class=\"pinned-item-desc color-fg-muted text-small mt-2 mb-0\">\n Axiom is a free, open source computer algebra system\n </p>\n\n <p class=\"mb-0 mt-2 f6 color-fg-muted\">\n <span class=\"tmp-mr-3 d-inline-block\">\n <span class=\"repo-language-color\" style=\"background-color: #da291c\"></span>\n <span itemprop=\"programmingLanguage\">PostScript</span>\n</span>\n\n <a href=\"/binghe/axiom-code/stargazers\" class=\"pinned-item-meta Link--muted\">\n <svg aria-label=\"stars\" role=\"img\" height=\"16\" viewBox=\"0 0 16 16\" version=\"1.1\" width=\"16\" data-view-component=\"true\" class=\"octicon octicon-star\">\n <path d=\"M8 .25a.75.75 0 0 1 .673.418l1.882 3.815 4.21.612a.75.75 0 0 1 .416 1.279l-3.046 2.97.719 4.192a.751.751 0 0 1-1.088.791L8 12.347l-3.766 1.98a.75.75 0 0 1-1.088-.79l.72-4.194L.818 6.374a.75.75 0 0 1 .416-1.28l4.21-.611L7.327.668A.75.75 0 0 1 8 .25Zm0 2.445L6.615 5.5a.75.75 0 0 1-.564.41l-3.097.45 2.24 2.184a.75.75 0 0 1 .216.664l-.528 3.084 2.769-1.456a.75.75 0 0 1 .698 0l2.77 1.456-.53-3.084a.75.75 0 0 1 .216-.664l2.24-2.183-3.096-.45a.75.75 0 0 1-.564-.41L8 2.694Z\"></path>\n</svg>\n 2\n </a>\n </p>\n "
]
}
{
"accept-ranges": "bytes",
"cache-control": "max-age=0, private, must-revalidate",
"content-encoding": "gzip",
"content-security-policy": "default-src 'none'; base-uri 'self'; child-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/; connect-src 'self' uploads.github.com www.githubstatus.com collector.github.com raw.githubusercontent.com api.github.com github-cloud.s3.amazonaws.com github-production-repository-file-5c1aeb.s3.amazonaws.com github-production-upload-manifest-file-7fdce7.s3.amazonaws.com github-production-user-asset-6210df.s3.amazonaws.com *.rel.tunnels.api.visualstudio.com wss://*.rel.tunnels.api.visualstudio.com github.githubassets.com objects-origin.githubusercontent.com copilot-proxy.githubusercontent.com proxy.individual.githubcopilot.com proxy.business.githubcopilot.com proxy.enterprise.githubcopilot.com *.actions.githubusercontent.com wss://*.actions.githubusercontent.com productionresultssa0.blob.core.windows.net productionresultssa1.blob.core.windows.net productionresultssa2.blob.core.windows.net productionresultssa3.blob.core.windows.net productionresultssa4.blob.core.windows.net productionresultssa5.blob.core.windows.net productionresultssa6.blob.core.windows.net productionresultssa7.blob.core.windows.net productionresultssa8.blob.core.windows.net productionresultssa9.blob.core.windows.net productionresultssa10.blob.core.windows.net productionresultssa11.blob.core.windows.net productionresultssa12.blob.core.windows.net productionresultssa13.blob.core.windows.net productionresultssa14.blob.core.windows.net productionresultssa15.blob.core.windows.net productionresultssa16.blob.core.windows.net productionresultssa17.blob.core.windows.net productionresultssa18.blob.core.windows.net productionresultssa19.blob.core.windows.net github-production-repository-image-32fea6.s3.amazonaws.com github-production-release-asset-2e65be.s3.amazonaws.com insights.github.com wss://alive.github.com wss://alive-staging.github.com api.githubcopilot.com api.individual.githubcopilot.com api.business.githubcopilot.com api.enterprise.githubcopilot.com; font-src github.githubassets.com; form-action 'self' github.com gist.github.com copilot-workspace.githubnext.com objects-origin.githubusercontent.com; frame-ancestors 'none'; frame-src viewscreen.githubusercontent.com notebooks.githubusercontent.com; img-src 'self' data: blob: github.githubassets.com media.githubusercontent.com camo.githubusercontent.com identicons.github.com avatars.githubusercontent.com private-avatars.githubusercontent.com github-cloud.s3.amazonaws.com objects.githubusercontent.com release-assets.githubusercontent.com secured-user-images.githubusercontent.com user-images.githubusercontent.com private-user-images.githubusercontent.com opengraph.githubassets.com marketplace-screenshots.githubusercontent.com copilotprodattachments.blob.core.windows.net/github-production-copilot-attachments/ github-production-user-asset-6210df.s3.amazonaws.com customer-stories-feed.github.com spotlights-feed.github.com objects-origin.githubusercontent.com *.githubusercontent.com; manifest-src 'self'; media-src github.com user-images.githubusercontent.com secured-user-images.githubusercontent.com private-user-images.githubusercontent.com github-production-user-asset-6210df.s3.amazonaws.com gist.github.com github.githubassets.com; script-src github.githubassets.com; style-src 'unsafe-inline' github.githubassets.com; upgrade-insecure-requests; worker-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/",
"content-type": "text/html; charset=utf-8",
"date": "Fri, 17 Apr 2026 16:29:26 GMT",
"etag": "591a18fc886d375e2b4ec7121ba5df68",
"referrer-policy": "origin-when-cross-origin, strict-origin-when-cross-origin",
"server": "github.com",
"set-cookie": "logged_in=no; expires=Sat, 17 Apr 2027 16:29:26 GMT; domain=.github.com; path=/; HttpOnly; secure; SameSite=Lax",
"strict-transport-security": "max-age=31536000; includeSubdomains; preload",
"transfer-encoding": "chunked",
"vary": "X-PJAX, X-PJAX-Container, Turbo-Visit, Turbo-Frame, X-Requested-With, Sec-Fetch-Site,Accept-Encoding, Accept, X-Requested-With",
"x-content-type-options": "nosniff",
"x-frame-options": "deny",
"x-github-request-id": "AA5C:13DA88:17042FE:1F81F0E:69E25FE4",
"x-xss-protection": "0"
}