Spaces:
Running
Running
Update extract.lean
Browse files- extract.lean +0 -5
extract.lean
CHANGED
|
@@ -55,11 +55,6 @@ def Lean.ConstantInfo.kind : ConstantInfo → String
|
|
| 55 |
| .ctorInfo _ => "constructor"
|
| 56 |
| .recInfo _ => "recursor"
|
| 57 |
|
| 58 |
-
/-
|
| 59 |
-
Turn Lean.Expr and related types into JSON.
|
| 60 |
-
-/
|
| 61 |
-
|
| 62 |
-
|
| 63 |
def truncatePrint (s : String) : IO Unit := do
|
| 64 |
IO.println (if s.length < 1000 then s else s.take 997 ++ " ...")
|
| 65 |
|
|
|
|
| 55 |
| .ctorInfo _ => "constructor"
|
| 56 |
| .recInfo _ => "recursor"
|
| 57 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 58 |
def truncatePrint (s : String) : IO Unit := do
|
| 59 |
IO.println (if s.length < 1000 then s else s.take 997 ++ " ...")
|
| 60 |
|