Open GoogleCodeExporter opened 8 years ago
Peter pointed out I'd given the wrong index. It should be:
> <= Fin.Ind ('suc m) i
But I guess it should give an error as the type of i isn't correct if you give
the wrong value for m.
Original comment by jmchap...@gmail.com
on 4 Sep 2010 at 7:56
The elaborator is very good at inserting coercions if you give it something
that isn't type-correct, but it is less good at spotting equations that are
impossible to solve. In particular, there is no cycle detection, so in this
case it probably inserted a few coercions by |m == 'suc m| (or more complicated
equations) and left them as hoping holes.
Original comment by adamgundry
on 6 Sep 2010 at 8:25
This is the output in full output in case it is useful:
Let there be wk.
\ m : Nat ->
\ n : Nat ->
\ f : (Fin m -> Fin n) ->
\ i : Fin ('suc m) ->
Programming: < wk^1 m n f i : Fin ('suc n) >
wk_2.impl_2 > <= Fin.Ind m i
Eliminated and simplified.
\ m^3 : Nat ->
\ n^2 : Nat ->
\ f^2 : (Fin m^3 -> Fin n^2) ->
\ i^3 : Fin ('suc m^3) ->
\ i^2 : Nat ->
\ s : Nat ->
\ qe : :- i^2 == ((: Nat) ('suc s)) ->
\ m : Nat ->
\ n^1 : Nat ->
\ f^1 : (Fin m -> Fin n^1) ->
\ i^1 : Fin ('suc m) ->
\ n : Nat ->
\ f : (Fin ('suc s) -> Fin n) ->
\ i : Fin ('suc ('suc s)) ->
\ qsm : :- ((: Fin ('suc s)) ('zero s)) == (coe Fin ('suc ('suc s)) Fin ('suc
s) (con [(\ s1 s2 fy -> [_ [[_ [_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch
['zero 'suc] xe (\ yb -> :- ((s2 : Enum ['zero 'suc]) => yb == s2 => eqGreen
Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig
())))] yb) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD
(Sig ())))] s2))) [(\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero
'suc]) 'zero) == yb => eqGreen Desc ('constD (Sig ())) Desc (switchD ['zero
'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _
, _]) (\ absurd -> naughtE (absurd %) (:- FF && FF && FF))]) (\ xe -> switch
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc
('prodD 'idD ('constD (Sig ()))) Desc (switchD ['zero 'suc] [('constD (Sig ()))
('prodD 'idD ('constD (Sig ())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF
&& FF && FF)) (\ _ -> [_ [_ , _] [_ _ , _] , _])])]) , _] , \ s2 s1 fy -> _] [_
[_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 :
Enum ['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD
(Sig ())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc]
[('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen
Desc ('constD (Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD
'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE
(absurd %) (:- FF && FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :-
(((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig
()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig
())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_
[_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> _) _ (fy %) , _]) [_ [_ _ [_ _
[_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 : Enum
['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD (Sig
())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc] [('constD
(Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch ['zero 'suc]
xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen Desc ('constD
(Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD
(Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE (absurd %) (:- FF &&
FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero
'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig ()))) Desc
(switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))]
yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_ [_ , _]
[_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [_ _ [_ _ [_ , _] , _] , _] [[_ [_
[_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 :
Enum ['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD
(Sig ())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc]
[('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen
Desc ('constD (Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD
'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE
(absurd %) (:- FF && FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :-
(((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig
()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig
())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_
[_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [(impl.eif.hope^4 ('suc s) n
f i s1^1 s2^1 fy^1 s1 s2 fy) , impl.eif.hope^3 ('suc s) n f i s1^1 s2^1 fy^1 s1
s2 fy] , _]) , _] [_ [_ [_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero
'suc] xe (\ yb -> :- ((s2 : Enum ['zero 'suc]) => yb == s2 => eqGreen Desc
(switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb)
Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig
())))] s2))) [(\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero
'suc]) 'zero) == yb => eqGreen Desc ('constD (Sig ())) Desc (switchD ['zero
'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _
, _]) (\ absurd -> naughtE (absurd %) (:- FF && FF && FF))]) (\ xe -> switch
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc
('prodD 'idD ('constD (Sig ()))) Desc (switchD ['zero 'suc] [('constD (Sig ()))
('prodD 'idD ('constD (Sig ())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF
&& FF && FF)) (\ _ -> [_ [_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [_
(fy %) , _] [_ [(impl.eif.hope^2 ('suc s) n f i s1^1 s2^1 fy^1 s1 s2 fy) ,
impl.eif.hope^1 ('suc s) n f i s1^1 s2^1 fy^1 s1 s2 fy] , _] , _]) , _] , _] ,
_]) , impl.eif.hope ('suc s) n f i %]) i) ->
Programming: < wk^1 ('suc s) n f i : Fin ('suc n) >
Original comment by jmchap...@gmail.com
on 6 Sep 2010 at 10:26
Original issue reported on code.google.com by
jmchap...@gmail.com
on 4 Sep 2010 at 7:30