A number list stored a set of numbers, the number value may be 0 or 1, no
other case, now, I want to get the value of n-th element of the list. If n
is greater than the length of the list,then fail. I don't know how to throw
the exception which defined by myself.
The function defined as follows:
val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l
>= SUC n) /\ (n >= 0)) then (if(n = 0) then (HD l) else NTH_BIT_VAL(n-1,TL
l)) else (failwith "n is greater than list's LENGTH")`;
Exception raised at TotalDefn.Define:
between line 40, character 31 and frag 0 row 0 col 137:
at TotalDefn.defnDefine:
The following variables are free in the
right hand side of the proposed definition: "failwith"
! Uncaught exception:
! HOL_ERR
val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l
>= SUC n) /\ (n >= 0)) then (if(n = 0) then (HD l) else NTH_BIT_VAL(n-1,TL
l)) else fail()`;
Exception raised at TotalDefn.Define:
on line 41, characters 30-159:
at TotalDefn.defnDefine:
The following variables are free in the
right hand side of the proposed definition: "fail"
! Uncaught exception:
! HOL_ERR
however, I define function using ML, done.
- fun nth_bit_val n l = if(n=0) then fail() else l;
> val 'a nth_bit_val = fn : int -> 'a -> 'a
thx
------------------------------------------------------------------------------
AlienVault Unified Security Management (USM) platform delivers complete
security visibility with the essential security capabilities. Easily and
efficiently configure, manage, and operate all of your security controls
from a single console and one unified framework. Download a free trial.
http://p.sf.net/sfu/alienvault_d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
