nil_app : forall (X : Type) (l : list X), [ ] ++ l = l
: forall (X : Type) (l : list X), [ ] ++ l = l
"coqc" -q -R "." Top -I "." P04.v
"coqc" -q -R "." Top -I "." E04_01.v
snoc_with_append
:
forall (X : Type) (l1 l2 : list X) (v : X),
snoc (l1 ++ l2) v = l1 ++ snoc l2 v
: forall (X : Type) (l1 l2 : list X) (v : X),
snoc (l1 ++ l2) v = l1 ++ snoc l2 v
"coqc" -q -R "." Top -I "." P05.v
@hd_opt
: forall X : Type, list X -> option X
"coqc" -q -R "." Top -I "." E05_01.v
conj test_hd_opt1 test_hd_opt2
:
hd_opt [1; 2] = Some 1 /\ hd_opt [[1]; [2]] = Some [1]
: hd_opt [1; 2] = Some 1 /\ hd_opt [[1]; [2]] = Some [1]
"coqc" -q -R "." Top -I "." Imp.v
File "./Imp.v", line 34, characters 15-19:
Error: Unable to locate library Maps.
make: *\ [Imp.vo] Error 1
rary Maps is required and has not been found in the loadpath!
"coqdep" -c -R "." Top -I "." "Smallstep.v" > "Smallstep.v.d" || ( RV=$?; rm -f "Smallstep.v.d"; exit ${RV} )
* Warning: in file Smallstep.v, library Maps is required and has not been found in the loadpath!
* Warning: in file Smallstep.v, library Maps is required and has not been found in the loadpath!
"coqdep" -c -R "." Top -I "." "SfLib.v" > "SfLib.v.d" || ( RV=$?; rm -f "SfLib.v.d"; exit ${RV} )
*\ Warning: in file Imp.v, library Maps is required and has not been found in the loadpath!
*\ Warning: in file Imp.v, library Maps is required and has not been found in the loadpath!
"coqdep" -c -R "." Top -I "." "E05_01.v" > "E05_01.v.d" || ( RV=$?; rm -f "E05_01.v.d"; exit ${RV} )
hestia49
commented
8 years ago
IDE를 이용한 Make 시 아래와 같이 오류가 납니다. Ass#2 까지는 문제 없이 메이크, 실행이 되었는데 Ass#3에서 오류가 납니다. 오류 전문은 다음과 같습니다.
Compilation output:
"coqdep" -c -R "." Top -I "." "Types.v" > "Types.v.d" || ( RV=$?; rm -f "Types.v.d"; exit ${RV} )
*\ Warning: in file Types.v, library Maps is required and has not been found in the loadpath!
*\ Warning: in file Types.v, lib"coqc" -q -R "." Top -I "." E02_01.v
test_repeat1 : repeat true 2 = [true; true] : repeat true 2 = [true; true]
"coqc" -q -R "." Top -I "." P03.v
"coqc" -q -R "." Top -I "." E03_01.v
nil_app : forall (X : Type) (l : list X), [ ] ++ l = l : forall (X : Type) (l : list X), [ ] ++ l = l
"coqc" -q -R "." Top -I "." P04.v
"coqc" -q -R "." Top -I "." E04_01.v
snoc_with_append : forall (X : Type) (l1 l2 : list X) (v : X), snoc (l1 ++ l2) v = l1 ++ snoc l2 v : forall (X : Type) (l1 l2 : list X) (v : X), snoc (l1 ++ l2) v = l1 ++ snoc l2 v
"coqc" -q -R "." Top -I "." P05.v
@hd_opt : forall X : Type, list X -> option X
"coqc" -q -R "." Top -I "." E05_01.v
conj test_hd_opt1 test_hd_opt2 : hd_opt [1; 2] = Some 1 /\ hd_opt [[1]; [2]] = Some [1] : hd_opt [1; 2] = Some 1 /\ hd_opt [[1]; [2]] = Some [1]
"coqc" -q -R "." Top -I "." Imp.v
File "./Imp.v", line 34, characters 15-19: Error: Unable to locate library Maps.
make: *\ [Imp.vo] Error 1
rary Maps is required and has not been found in the loadpath! "coqdep" -c -R "." Top -I "." "Smallstep.v" > "Smallstep.v.d" || ( RV=$?; rm -f "Smallstep.v.d"; exit ${RV} )
* Warning: in file Smallstep.v, library Maps is required and has not been found in the loadpath! * Warning: in file Smallstep.v, library Maps is required and has not been found in the loadpath! "coqdep" -c -R "." Top -I "." "SfLib.v" > "SfLib.v.d" || ( RV=$?; rm -f "SfLib.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "P05.v" > "P05.v.d" || ( RV=$?; rm -f "P05.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "P04.v" > "P04.v.d" || ( RV=$?; rm -f "P04.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "P03.v" > "P03.v.d" || ( RV=$?; rm -f "P03.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "P02.v" > "P02.v.d" || ( RV=$?; rm -f "P02.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "P01.v" > "P01.v.d" || ( RV=$?; rm -f "P01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "Imp.v" > "Imp.v.d" || ( RV=$?; rm -f "Imp.v.d"; exit ${RV} )
*\ Warning: in file Imp.v, library Maps is required and has not been found in the loadpath!
*\ Warning: in file Imp.v, library Maps is required and has not been found in the loadpath! "coqdep" -c -R "." Top -I "." "E05_01.v" > "E05_01.v.d" || ( RV=$?; rm -f "E05_01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "E04_01.v" > "E04_01.v.d" || ( RV=$?; rm -f "E04_01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "E03_01.v" > "E03_01.v.d" || ( RV=$?; rm -f "E03_01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "E02_01.v" > "E02_01.v.d" || ( RV=$?; rm -f "E02_01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "E01_02.v" > "E01_02.v.d" || ( RV=$?; rm -f "E01_02.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "E01_01.v" > "E01_01.v.d" || ( RV=$?; rm -f "E01_01.v.d"; exit ${RV} )
"coqdep" -c -R "." Top -I "." "D.v" > "D.v.d" || ( RV=$?; rm -f "D.v.d"; exit ${RV} )
"coqc" -q -R "." Top -I "." D.v
"coqc" -q -R "." Top -I "." P01.v
"coqc" -q -R "." Top -I "." E01_01.v
test_split : split [(1, false); (2, false)] = ([1; 2], [false; false]) : split [(1, false); (2, false)] = ([1; 2], [false; false])
"coqc" -q -R "." Top -I "." E01_02.v
split_map : forall (X Y : Type) (l : list (X * Y)), fst (split l) = map fst l : forall (X Y : Type) (l : list (X * Y)), fst (split l) = map fst l
"coqc" -q -R "." Top -I "." P02.v