some cleanup

teorth · Sep 29, 2024 · c79830c · c79830c
1 parent 2c2edcf
commit c79830c
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 deletions.
diff --git a/equational_theories/Conjecture.lean b/equational_theories/Conjecture.lean
@@ -26,7 +26,8 @@ inductive EntryVariant where
 structure Entry where
 /-- Name of the declaration. -/
 (name : Name)
-/-- Lean code to be included in the extracted problem file. -/
+
+/-- Which kind of conjecture is it? -/
 (variant : EntryVariant)
 
 initialize conjectureExtension : SimplePersistentEnvExtension Entry (Array Entry) ←

diff --git a/equational_theories/Result.lean b/equational_theories/Result.lean
@@ -7,24 +7,27 @@ open Lean Parser Elab Command
 
 namespace Result
 
+/--
+A theorem providing an implication or negated implication to our directed graph.
+-/
 syntax (name := result) declModifiers "result " declId ppIndent(declSig) declVal : command
 
-/-- An entry in the conjecture environment extension.
+/-- An entry in the result environment extension.
 -/
 inductive EntryVariant where
   | implication : Implication → EntryVariant
   | nonimplication : Implication → EntryVariant
+deriving Lean.ToJson, Lean.FromJson
 
-/-- An entry in the conjecture environment extension -/
+/-- An entry in the result environment extension -/
 structure Entry where
 /-- Name of the declaration. -/
 (name : Name)
-
 /-- Name of the file where this declaration was found. -/
 (filename : String)
-
-/-- Lean code to be included in the extracted problem file. -/
+/-- Which kind of result is it? -/
 (variant : EntryVariant)
+deriving Lean.ToJson, Lean.FromJson
 
 initialize resultExtension : SimplePersistentEnvExtension Entry (Array Entry) ←
   registerSimplePersistentEnvExtension {
@@ -36,7 +39,7 @@ initialize resultExtension : SimplePersistentEnvExtension Entry (Array Entry)
 /-- Elaborates a `result` declaration.
 -/
 elab_rules : command
-| `(command| $dm:declModifiers result%$rs $di:declId $ds:declSig $dv:declVal) => do
+| `(command| $dm:declModifiers result $di:declId $ds:declSig $dv:declVal) => do
   let filename := (←read).fileName
   let modifiers ← elabModifiers dm
   let expanded_decl_id ← expandDeclId di modifiers
@@ -66,7 +69,7 @@ def extractResults {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] :
     m (Array Entry) := do
   return resultExtension.getState (← getEnv)
 
-/-- Prints the contents of the conjecture environment extension.
+/-- Prints the contents of the result environment extension.
 -/
 syntax (name := printResults) "#print_results" : command