Lean4 style #eval command?

[spaceunifyfifty]

I see that there is a way to check the type of a term from within source, is there a way to compute an expression and display it's result like Lean's #eval does? If not, could this be feasible to add at some point?

[mtzguido]

Not yet but coming soon! #4132.

[mtzguido]

This will be available in the next F* release, or already there if you build the fstar2 branch.