{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "e242e178-f985-4edd-be33-4a4a35ee0b8b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "        \n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/alectryon.css\">\n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/pygments.css\">\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/alectryon.js\"></script>\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/highlight.js\"></script>\n",
       "        <style>\n",
       "            @media (any-hover: hover) {\n",
       "                .alectryon-io .alectryon-sentence:hover .alectryon-output,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {\n",
       "                    position: unset;\n",
       "                }\n",
       "            }\n",
       "\n",
       "            .highlight .w, .code .w {\n",
       "                color: #d3d7cf;\n",
       "                text-decoration: none;\n",
       "            }\n",
       "\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goals,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-messages,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goal,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-message {\n",
       "                background: black;\n",
       "            }\n",
       "        </style>\n",
       "    \n",
       "        <div class=\"alectryon-root alectryon-centered\">\n",
       "            <pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"c1\">--%cd .</span></span></span></pre>\n",
       "<pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"c1\">--% env 0</span></span></span></pre>\n",
       "        </div>\n",
       "        <details>\n",
       "            <summary>Raw input</summary>\n",
       "            <code>{\"cmd\": \"--%cd .\"}</code>\n",
       "        </details>\n",
       "        <details>\n",
       "            <summary>Raw output</summary>\n",
       "            <code>{\"env\": 0}</code>\n",
       "        </details>\n",
       "    "
      ],
      "text/plain": [
       "--%cd .\n",
       "--% env 0\n",
       "\n",
       "Raw input:\n",
       "{\"cmd\": \"--%cd .\"}\n",
       "Raw output:\n",
       "{\"env\": 0}"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "%cd ."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "a3f6d8bf-4710-4d45-912e-ffd28639181c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "        \n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/alectryon.css\">\n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/pygments.css\">\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/alectryon.js\"></script>\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/highlight.js\"></script>\n",
       "        <style>\n",
       "            @media (any-hover: hover) {\n",
       "                .alectryon-io .alectryon-sentence:hover .alectryon-output,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {\n",
       "                    position: unset;\n",
       "                }\n",
       "            }\n",
       "\n",
       "            .highlight .w, .code .w {\n",
       "                color: #d3d7cf;\n",
       "                text-decoration: none;\n",
       "            }\n",
       "\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goals,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-messages,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goal,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-message {\n",
       "                background: black;\n",
       "            }\n",
       "        </style>\n",
       "    \n",
       "        <div class=\"alectryon-root alectryon-centered\">\n",
       "            <pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"c1\">--%cd demo_proj</span></span></span></pre>\n",
       "<pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"kn\">import</span><span class=\"w\"> </span><span class=\"bp\">«</span>DemoProj<span class=\"bp\">»</span></span></span></pre>\n",
       "<pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"c1\">--% env 0</span></span></span></pre>\n",
       "        </div>\n",
       "        <details>\n",
       "            <summary>Raw input</summary>\n",
       "            <code>{\"cmd\": \"--%cd demo_proj\\nimport \\u00abDemoProj\\u00bb\"}</code>\n",
       "        </details>\n",
       "        <details>\n",
       "            <summary>Raw output</summary>\n",
       "            <code>{\"env\": 0}</code>\n",
       "        </details>\n",
       "    "
      ],
      "text/plain": [
       "--%cd demo_proj\n",
       "import «DemoProj»\n",
       "--% env 0\n",
       "\n",
       "Raw input:\n",
       "{\"cmd\": \"--%cd demo_proj\\nimport \\u00abDemoProj\\u00bb\"}\n",
       "Raw output:\n",
       "{\"env\": 0}"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "%cd demo_proj\n",
    "import «DemoProj»"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "31e5eec2-1eb3-4736-94d5-826fd0fd6d24",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "        \n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/alectryon.css\">\n",
       "        <link rel=\"stylesheet\" href=\"https://lean-lang.org/lean4/doc/pygments.css\">\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/alectryon.js\"></script>\n",
       "        <script src=\"https://lean-lang.org/lean4/doc/highlight.js\"></script>\n",
       "        <style>\n",
       "            @media (any-hover: hover) {\n",
       "                .alectryon-io .alectryon-sentence:hover .alectryon-output,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,\n",
       "                .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {\n",
       "                    position: unset;\n",
       "                }\n",
       "            }\n",
       "\n",
       "            .highlight .w, .code .w {\n",
       "                color: #d3d7cf;\n",
       "                text-decoration: none;\n",
       "            }\n",
       "\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goals,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-messages,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-goal,\n",
       "            body[data-jp-theme-light=\"false\"] .alectryon-io .alectryon-message {\n",
       "                background: black;\n",
       "            }\n",
       "        </style>\n",
       "    \n",
       "        <div class=\"alectryon-root alectryon-centered\">\n",
       "            <pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><input class=\"alectryon-toggle\" id=\"chk0\" style=\"display: none\" type=\"checkbox\"><label class=\"alectryon-input\" for=\"chk0\"><span class=\"bp\">#</span>check<span class=\"w\"> </span>CliffordAlgebra</label><small class=\"alectryon-output\"><div><div class=\"alectryon-messages\"><blockquote class=\"alectryon-message\"> CliffordAlgebra<span class=\"bp\">.</span>{u_2,<span class=\"w\"> </span>u_1}<span class=\"w\"> </span>{R<span class=\"w\"> </span>:<span class=\"w\"> </span><span class=\"kt\">Type</span><span class=\"w\"> </span>u_1}<span class=\"w\"> </span>[CommRing<span class=\"w\"> </span>R]<span class=\"w\"> </span>{M<span class=\"w\"> </span>:<span class=\"w\"> </span><span class=\"kt\">Type</span><span class=\"w\"> </span>u_2}<span class=\"w\"> </span>[AddCommGroup<span class=\"w\"> </span>M]<span class=\"w\"> </span>[Module<span class=\"w\"> </span>R<span class=\"w\"> </span>M]\n",
       "<span class=\"w\">  </span>(Q<span class=\"w\"> </span>:<span class=\"w\"> </span>QuadraticForm<span class=\"w\"> </span>R<span class=\"w\"> </span>M)<span class=\"w\"> </span>:<span class=\"w\"> </span><span class=\"kt\">Type</span><span class=\"w\"> </span>(max<span class=\"w\"> </span>u_2<span class=\"w\"> </span>u_1)</blockquote></div></div></small></span></pre>\n",
       "<pre class=\"alectryon-io highlight\"><!-- Generator: Alectryon --><span class=\"alectryon-sentence\"><span class=\"alectryon-input\"><span class=\"c1\">--% env 1</span></span></span></pre>\n",
       "        </div>\n",
       "        <details>\n",
       "            <summary>Raw input</summary>\n",
       "            <code>{\"cmd\": \"#check CliffordAlgebra\", \"env\": 0}</code>\n",
       "        </details>\n",
       "        <details>\n",
       "            <summary>Raw output</summary>\n",
       "            <code>{\"messages\":\r\n",
       " [{\"severity\": \"info\",\r\n",
       "   \"pos\": {\"line\": 1, \"column\": 0},\r\n",
       "   \"endPos\": {\"line\": 1, \"column\": 6},\r\n",
       "   \"data\":\r\n",
       "   \"CliffordAlgebra.{u_2, u_1} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]\\n  (Q : QuadraticForm R M) : Type (max u_2 u_1)\"}],\r\n",
       " \"env\": 1}</code>\n",
       "        </details>\n",
       "    "
      ],
      "text/plain": [
       "#check CliffordAlgebra\n",
       "──────▶  CliffordAlgebra.{u_2, u_1} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]\n",
       "  (Q : QuadraticForm R M) : Type (max u_2 u_1)\n",
       "--% env 1\n",
       "\n",
       "Raw input:\n",
       "{\"cmd\": \"#check CliffordAlgebra\", \"env\": 0}\n",
       "Raw output:\n",
       "{\"messages\":\r\n",
       " [{\"severity\": \"info\",\r\n",
       "   \"pos\": {\"line\": 1, \"column\": 0},\r\n",
       "   \"endPos\": {\"line\": 1, \"column\": 6},\r\n",
       "   \"data\":\r\n",
       "   \"CliffordAlgebra.{u_2, u_1} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]\\n  (Q : QuadraticForm R M) : Type (max u_2 u_1)\"}],\r\n",
       " \"env\": 1}"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "#check CliffordAlgebra"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Lean 4",
   "language": "lean4",
   "name": "lean4"
  },
  "language_info": {
   "codemirror_mode": "python",
   "file_extension": ".lean",
   "mimetype": "text/x-lean4",
   "name": "lean4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}