git.iko.soy/Idris-dev
on master help sign in
Error message tinker
commit8baaa424e36a96bc3697deb85e6b89a8d3d9636f authorEdwin Brady <edwin@zoot.local> dateTue 24 Jan 2012, 15:20 (15 years ago) parentae4be75
4 files changed+13−6
compare with master
unifiedsplit
CHANGELOG+4 idris.cabal+2−2 src/Idris/Delaborate.hs+6−3 tutorial/examples/Makefile+1−1
CHANGELOG+4
@@ -1,3 +1,7 @@
1+New in 0.9.1:
2+
3+* dsl notation
4+
150.1.x to 0.9.0:
26
37Complete rewrite. User visible changes:
idris.cabal+2−2
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 0.9.0
2+Version: 0.9.1
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -8,7 +8,7 @@ Homepage: http://www.idris-lang.org/
88
99Stability: Beta
1010Category: Compilers/Interpreters, Dependent Types
11−Synopsis: Dependently Typed Functional Programming Language
11+Synopsis: Functional Programming Language with Dependent Types
1212Description: Idris is a general purpose language with full dependent types.
1313 It is compiled, with eager evaluation.
1414 Dependent types allow types to be predicated on values,
src/Idris/Delaborate.hs+6−3
@@ -64,9 +64,12 @@ delab' ist tm fullname = de [] tm
6464
6565pshow :: IState -> Err -> String
6666pshow i (Msg s) = s
67−pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)
68− ++ " with " ++ show (delab i y)
69−-- ++ "\n\t(" ++ pshow i e ++ ")"
67+pshow i (CantUnify x y e s)
68+ = "Can't unify " ++ show (delab i x)
69+ ++ " with " ++ show (delab i y) ++
70+ case e of
71+ Msg "" -> ""
72+ _ -> "\n\nSpecifically:\n\t " ++ pshow i e
7073pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
7174 " when unifying " ++ show (delab i x) ++ " and " ++
7275 show (delab i y)
tutorial/examples/Makefile+1−1
@@ -1,5 +1,5 @@
11check: .PHONY
2− rm *.ibc
2+ rm -f *.ibc
33 for x in *.idr ; do \
44 echo "Checking $$x"; \
55 idris --check $$x; \