Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Fix refine bug

  • Loading branch information...
commit 23d8bc68d705c2e11009f137edb3f5eced84d960 1 parent 21dcadb
Edwin Brady authored
Showing with 2 additions and 0 deletions.
  1. +2 −0  Ivor/Tactics.lhs
2  Ivor/Tactics.lhs
View
@@ -360,6 +360,8 @@ names. Let's record which ones...
> mkns (UN a) (UN b) = UN (a++"_"++b)
> mkns (MN (a,i)) (UN b) = MN (a++"_"++b, i)
> mkns (MN (a,i)) (MN (b,j)) = MN (a++"_"++b, i)
+> mkns (UN b) (MN (a,i)) = MN (b++"_"++a, i)
+> mkns x y = error $ "FAIL: " ++ show (x,y)
> doClaims :: Name -> [((Name, TT Name), Maybe (TT Name))] -> Tactic
> doClaims h [] gam env tm = tacret $ tm
Please sign in to comment.
Something went wrong with that request. Please try again.