Per

[vrahli]

Added per types, defined a new squash operator using per, proved that it's equivalent to the one that uses the image type, defined quotient types using per, and proved their well-formedness.

[jozefg]

I think there's a small bug, in tactic.sml there should be a new case of branchSubst to handle UNHIDE. Maybe?

[jonsterling]

@jozefg Yes, that is correct.

• [x] @vrahli would you please add a new clause in tactic.sml/branchSubst for unhide? thanks!

[vrahli]

Do you mean substBranch in src/syntax/tactic.sml? What's that function doing? On Sep 3, 2015 3:35 PM, "Jonathan Sterling" notifications@github.com wrote:

@jozefg https://github.com/jozefg Yes, that is correct.

• @vrahli https://github.com/vrahli would you please add a new clause in tactic.sml/branchSubst for unhide? thanks!

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/pull/227#issuecomment-137467831.

[jozefg]

@vrahli When a Match tactic gets a substitution, it uses that to push the substitution through the tactic it's supposed to run. So that has to take a substitution and ensure that it is applied to every occurrence of a variable or term in a tactic. We can't do this with abts because they're a little too simple to handle binding term variables in tactics and such.

It's pretty messy, I think I'm going to get rid of that catch-all case because it makes these bugs way too easy.

[vrahli]

I've added a case in substBranch and per.jonprl now imports from other files via per.cfg.

[jonsterling]

Excellent, thanks! I'll look through it tonight and merge. Very exciting!