A repl command to run double checker on a function definition

[ice1000]

[HoshinoTented]

how to do

[ice1000]

how to do

The first step is to extend the double checker so it can double-check a function definition. This requires double-checking clauses. Then, we add a repl command similar to :i someDef and it runs the double checker on someDef.