idris-lang/Idris-dev — pull request #924 by david-christiansen (2014-02-23 20:54:55+00:00)
Title: Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands:

* :t, :type gives the type of an expression
* :e, :eval normalises the expression and prints the result

These work within the proof environment, so evaluating expressions that
contain references to hypotheses is allowed.

Fixes #505.