Dear All,
I am having the following type checking issue with a definition in the
Matrix theory of HOL-Light. It seems the double application of the function
leads to an unknown dimension of the matrix, which is causing the problem.
I would appreciate if someone can please help me out with us.
let horz_conct1 = new_definition
`(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda
a b .
if (b<=dimindex(:N))
then (A$a$b) else (B$a$(b-(dimindex(:N))))`;;
Now if i want to prove that
g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B)
(C)= horz_conct1 (A) (horz_conct1 B C)`;;
it gives following error
Exception: Failure "typechecking error (initial type assignment)".
So the definition is accepted but the proof goal using the function gives
the problem.
Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
