The Coq mailing list

[postmaster AT postech.ac.kr]

Transmit Report:

genilhs AT postech.ac.kr¿¡°Ô
 ¸ÞÀÏ ¹ß¼ÛÀ» 3¹ø ½ÃµµÇßÁö¸¸ ½ÇÆÐÇÏ¿´½À´Ï´Ù.
(½ÇÆÐ ÀÌÀ¯ : 550 
genilhs AT postech.ac.kr
 User unknown. 
(WhiteIP=N,AuthPass=N,SMTP_INBOUND_ONLY=N,ToLocalDomain=Y,ToUnknown=Y)(141.223.1.1))

<Âü°í> ½ÇÆÐ ÀÌÀ¯¿¡ ´ëÇÑ ¼³¸í
User unknown       :¸ÞÀÏÀ» ¼ö½ÅÇÒ »ç¿ëÀÚ°¡ Á¸ÀçÇÏÁö ¾ÊÀ½
Socket connect fail:¼ö½Å ¸ÞÀÏ ¼­¹ö¿Í ¿¬°á ½ÇÆÐ
DATA write fail    :¼ö½Å ¸ÞÀÏ ¼­¹ö·Î ¸Þ¼¼Áö ¼Û½Å ½ÇÆÐ
DATA reponse fail  :¼ö½Å ¸ÞÀÏ ¼­¹ö·ÎºÎÅÍ ¸Þ¼¼Áö ¼ö½Å ½ÇÆÐ
Reporting-MTA: dns; postech.ac.kr

Final-Recipient: rfc822;genilhs AT postech.ac.kr
Diagnostic-Code: smtp; 550 error - genilhs AT postech.ac.kr User unknown. (WhiteIP=N,AuthPass=N,SMTP_INBOUND_ONLY=N,ToLocalDomain=Y,ToUnknown=Y)(141.223.1.1)
Action: failed
Status: 5.0.0

--- Begin Message ---

• From: Adam Chlipala <adamc AT csail.mit.edu>
• To: Ömer Sinan Ağacan <omeragacan AT gmail.com>
• Cc: coq-club AT inria.fr
• Subject: Re: [Coq-Club] how to write this function?
• Date: Sat, 05 Apr 2014 15:38:06 -0400
• List-archive: <http://sympa.inria.fr/sympa/arc/coq-club>
• List-id: <coq-club.inria.fr>

It sounds to me like you're getting into territory where ad-hoc answers on a mailing list won't be very effective. An introduction to programming with dependent types in Coq (e.g., CPDT <http://adam.chlipala.net/cpdt/>) is probably worth reading.

On 04/05/2014 03:34 PM, Ömer Sinan Ağacan wrote:

Thanks for your answer! I tried using eq_nat_dec without using lemmas,
just to see how error will change and how does that help Coq inferring
stop = n, but it's still giving same error message:

Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
triangle_t T idx) : Vector.t T stop :=
if eq_nat_dec idx stop then
match tr with triangle _ _ v _ => v end
else
match tr with triangle _ _ _ tr' => nth_triangle_aux (S idx) stop tr'
end.

Error:
In environment
nth_triangle_aux : forall (T : Type) (idx stop : nat),
triangle_t T idx -> Vector.t T stop
T : Type
idx : nat
stop : nat
tr : triangle_t T idx
e : idx = stop
T0 : Type
n : nat
v : Vector.t T0 n
t : triangle_t T0 (S n)
The term "v" has type "Vector.t T0 n" while it is expected to have type
"Vector.t ?23 stop".

Is there anything else I need to do for telling Coq that stop = n?

--- End Message ---