search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

by-apply: allow partial args using #:with #122

Closed stchang closed 4 years ago

stchang commented 4 years ago

The unspecified args should be subgoals

from @dmelcer9

stchang commented 4 years ago

And if inference fails, it should also add the remaining unsolved antecedents as subgoals