diff --git a/TODO.md b/TODO.md index 890eba9..c94422f 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,7 @@ ## TODO +- [ ] unsolved meta errors repeat (need to freeze at some point) - [x] Sanitize JS idents, e.g. `_+_` - [ ] Generate some programs that do stuff - [x] import diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 22ca115..5c5c740 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -143,8 +143,8 @@ parameters (ctx: Context) if (length sp /= size) then do -- need INFO that works like debug. -- FIXME we probably need to hold onto the constraint and recheck when we solve the meta? - info (getFC t) "meta \{show m} applied to \{show $ length sp} args insted of \{show size}" - -- error (getFC t) "meta \{show m} applied to \{show $ length sp} args insted of \{show size}" + info (getFC t) "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" + -- error (getFC t) "meta \{show m} applied to \{show $ length sp} args instead of \{show size}" else do debug "meta \{show meta}" ren <- invert l sp diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 35287a8..1de488f 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -39,7 +39,7 @@ Eq BD where Defined == Defined = True _ == _ = False - +public export Show BD where show Bound = "bnd" show Defined = "def" diff --git a/tests/black/Zoo4eg.newt b/tests/black/Zoo4eg.newt index b38e2bf..17e103e 100644 --- a/tests/black/Zoo4eg.newt +++ b/tests/black/Zoo4eg.newt @@ -56,15 +56,15 @@ list1 : List Bool list1 = cons true (cons false (cons true nil)) -- dependent function composition -comp : {A} {B : A -> U} {C : {a} -> B a -> U} - (f : {a} (b : B a) -> C b) +comp : {A} {B : A -> U} {C : {a : A} -> B a -> U} + (f : {a : A} (b : B a) -> C b) (g : (a : A) -> B a) (a : A) -> C (g a) comp = \f g a => f (g a) -compExample : _ -compExample = comp (cons true) (cons false) nil +-- compExample : Bool +-- compExample = comp (cons true) (cons false) nil Nat : U Nat = (N : U) -> (N -> N) -> N -> N