search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Targeted Reduce and Unfold #208

Open jozefg opened 9 years ago

jozefg commented 9 years ago

Currently reduce and Unfold globally apply their transformations. Instead they should be able to optionally take a path (for example, [h. =(foo; bar; h)]) and then only apply their transformations at that spot.

jonsterling commented 9 years ago

:+1: Additionally, it should be possible to specify a target such that it only rewrites in a certain hypothesis, or in the conclusion, etc.