search

snu-sf-class / pl2016

14 stars 17 forks source link

Assignment 04 #50

Open jeehoonkang opened 8 years ago

jeehoonkang commented 8 years ago

Assignment 04 is issued: https://github.com/snu-sf-class/pl2016#assignments

Please ask questions here.

nolsigan commented 8 years ago

In P01.v split, when I try to match l with [] and result []*[], coq gives me an error

The term "[]" has type "list ?2" while it is expected to have type "nat".

Am I doing something wrong?

Fixpoint split                                                                        
            {X Y : Type} (l : list (X*Y))                                              
            : (list X) * (list Y) :=                                                   
 match l with                                                                        
 | [] => ([] * [])
shuuki4 commented 8 years ago

' * ' 가 type_scope 로 정의된 notation이라 coq가 *를 prod로 안받아들여서 그런거 아닌가요? ([], []) 로 하시면 될거같아요.

nolsigan commented 8 years ago

감사합니다!