Skip to content

Commit

Permalink
Commenting unnecessary eval statements
Browse files Browse the repository at this point in the history
  • Loading branch information
JOSHCLUNE committed Jun 20, 2024
1 parent 91cd0e8 commit 5a2ce7c
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 2 deletions.
2 changes: 2 additions & 0 deletions Auto/Parser/LexInit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -144,13 +144,15 @@ def term : ERE := .plus #[
]

-- Good property: Each state have at most one attribute!
/-
#eval string.toADFA
#eval specConst.toADFA
#eval sexpr.toADFA
#eval identifier.toADFA -- State 6 has two attributes, not sure if that's a problem
#eval sort.toADFA -- State 6 has two attributes, not sure if that's a problem
#eval sorted_var.toADFA -- State 6 has two attributes, not sure if that's a problem
#eval term.toADFA -- States 9, 36, and 37 have multiple attributes, not sure if that's a problem
-/

local instance : Hashable Char where
hash c := hash c.val
Expand Down
4 changes: 2 additions & 2 deletions Auto/Translation/Inductive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ def collectExprsSimpleInduct (es : Array Expr) : MetaM (Array (Array SimpleIndVa
end Auto

section Test

/-
private def skd (e : Expr) : Elab.Term.TermElabM Unit := do
let (_, st) ← (Auto.collectExprSimpleInduct (Auto.Expr.eraseMData e)).run {}
for siw in st.sis do
Expand Down Expand Up @@ -202,5 +202,5 @@ section Test
end
#getExprAndApply[Tree Int|skd]

-/
end Test

0 comments on commit 5a2ce7c

Please sign in to comment.