Is there function for normalizing a term in elaboration m?

Stream: Is there code for X?

[Alissa Tung]

Hello, I am trying to find a function for normalizing a term in elaboration monad. Or evaluation function for expressions. I had tried some search and read the implementation for command eval, but I have not find something can be used in elab m.

[Alissa Tung]

I had tried something like

elab "debug!" x:term : term => do
  logInfo x
  let xs <- elabTermAndSynthesize x .none
  logInfo xs
  logInfo (<- eval% xs)
  return xs

but seems is not correct

(kernel) declaration has free variables '_tmp._@.Main._hyg.144'

[Eric Wieser]

What do you mean by "normalize"?

[Alissa Tung]

Eric Wieser said:

What do you mean by "normalize"?

Sorry I am not familiar with the terms, the two terms I used here are

• normalize: syntax -> syntax, which is elaborates the syntax to expression, run the reduction or calculations, read back to syntax

• evaluate: expression -> expression, simplify the expression, for example, calculate function applications