<pango>
bla: when you pattern-match against a variable, the variable is locally defined with the value it's unified with
<mbishop>
Anyone know if the cothreads guy gets on IRC?
<pango>
bla: so you you pattern match a value with zero, it redefines zero
<pango>
s/you/you/when you/
<pango>
# let a = 3 in match 2 with a -> a ;;
<pango>
Warning Y: unused variable a.
<pango>
- : int = 2
<mbishop>
anyone know if Zheng Li gets on IRC?
<bla>
Hm.
<bla>
I see
<bla>
Right.
<bla>
Stupid me.
<pango>
maybe match sign_n, sign_m with | 0, 0 -> ... etc.
<bla>
It will suffice if I place there 'Int 0' instead of giving it name at first.
dbueno has quit ["This computer has gone to sleep"]
<bla>
(;
<bla>
It even works actually.
<bla>
But slowly. I need to find a way to easily add there memoizing so it will get linear.
<EliasAmaral>
psnively, something extractable?
<psnively>
Yes: it might be fun to propose a strongly-specified function, develop it in Coq, then extract Scheme, OCaml, or Haskell code for it.
<EliasAmaral>
Hmmmm. Yeah, I read Coq can generate code =o but, the problem begins with the question "what function?". I will try to search a bit, thanks :)
<ita>
if you just want to give more specifications to functions, a preprocessor for giving contracts might be a better idea
<ita>
with coq it is necessary to do all the program in it (or a whole algorithm), not just one or two functions
<psnively>
ita: Actually, you can extract just a module for some of its targets.
postalchris has quit ["Leaving."]
<EliasAmaral>
i don't want something specific to be done, i wanted just some ideas to do with this kind of technology
<bla>
Uch. I find only problems today.
<bla>
Can I have a two dimensional array of Nums (arbitraly precision objects)?
<ita>
bla: like a matrix ?
<EliasAmaral>
i heard that you can use coq to prove things about programs, but that is too.. vague. there must be something practical to do with theorem provers
ita has quit [Remote closed the connection]
<psnively>
Um, proving things about programs IS practical.
<pango>
Num.num array array ?
<bla>
So with normal Array module rather then Array2...
<bla>
So I'll try once again.
ita has joined #ocaml
<pango>
"This module implements multi-dimensional arrays of integers and floating-point numbers"... Hence not of big_ints
<EliasAmaral>
psnively, but, but.. well, what things? an example :~ something simple but useful
<pango>
that are always boxed
<bla>
Array.make_matrix oh. Found.
<bla>
Array.init 20 (fun a -> Array.make 20);; just wouldn't work. :)
<psnively>
EliasAmaral: OK. How about a strongly-specified sort function?
<EliasAmaral>
ok, what exactly is a strongly-specified function? a function that has formal requirements/constraints?
<psnively>
A function whose return type defines what the function does.
<psnively>
In this case, a function whose return type specifies that the result is sorted.