Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Use 'Just' rather than 'just'

darcs-hash:20090305165807-228f4-c8a1925586f490e4f69d2a057985915717a480fa.gz
  • Loading branch information...
commit 69323bd5f11a8c86e59fa3d8e3ed59be1db74ffc 1 parent 4ebcbec
eb authored
Showing with 4 additions and 4 deletions.
  1. +3 −3 Ivor/Construction.lhs
  2. +1 −1  Ivor/TTCore.lhs
View
6 Ivor/Construction.lhs
@@ -79,7 +79,7 @@ check that there is the right number (num).
> -- | Try to solve a goal @A@ by evaluating a term of type @Maybe A@. If the
-> -- answer is @just a@, fill in the goal with the proof term @a@.
+> -- answer is @Just a@, fill in the goal with the proof term @a@.
> isItJust :: IsTerm a => a -> Tactic
> isItJust tm g ctxt = do
> gd <- goalData ctxt False g
@@ -90,9 +90,9 @@ check that there is the right number (num).
> case ty of
> (App (Name _ m) a) | m == (name "Maybe")
> -> do case prf of
-> (App (Name _ n) _) | n == (name "nothing")
+> (App (Name _ n) _) | n == (name "Nothing")
> -> fail "No solution found"
-> (App (App (Name _ j) _) p) | j == (name "just")
+> (App (App (Name _ j) _) p) | j == (name "Just")
> -> fill p g ctxt
> tm -> fail $ "Evaluated to " ++ show tm
> _ -> fail $ "Type of decision procedure must be ++ " ++
View
2  Ivor/TTCore.lhs
@@ -478,7 +478,7 @@ a complete definition.
Return all the names used in a scope
-> getNames :: Eq n => Scope (TT n) -> [n]
+> getNames :: (Show n, Eq n) => Scope (TT n) -> [n]
> getNames (Sc x) = nub $ p' x where
> p' (P x) = [x]
> p' (App f' a) = (p' f')++(p' a)
Please sign in to comment.
Something went wrong with that request. Please try again.