In [1]:

%cd .

--%cd .

--% env 0

Raw input

{"cmd": "--%cd ."}

Raw output

{"env": 0}

In [2]:

%cd demo_proj
import «DemoProj»

--%cd demo_proj

import «DemoProj»

--% env 0

Raw input

{"cmd": "--%cd demo_proj\nimport \u00abDemoProj\u00bb"}

Raw output

{"env": 0}

In [3]:

#check CliffordAlgebra

#check CliffordAlgebra CliffordAlgebra.{u_2, u_1} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) : Type (max u_2 u_1)

--% env 1

Raw input

{"cmd": "#check CliffordAlgebra", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "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)"}],
 "env": 1}