Howdy,
ri...@happyleptic.org skribis:
> but I
> understand that you could be very interested in Coq proving that a
> complex recursive algorithm eventually terminates, while you don't care
> much about the type checking.
Actually, I just meant to say that type-checking is one of the many
checks
Hey!
MIT/GNU Scheme provides a very nice user interface for this:
1 ]=> foo
;Unbound variable: foo
;To continue, call RESTART with an option number:
; (RESTART 3) => Specify a value to use instead of foo.
; (RESTART 2) => Define foo to a given value.
; (RESTART 1) => Return to read-e
On Fri 14 Oct 2011 18:30, Linas Vepstas writes:
> Let me demonstrate my ignorance: what pattern-matching srfi
> should I be using?
See "Pattern Matching" in the manual.
Andy
--
http://wingolog.org/
On 14 October 2011 03:28, Andy Wingo wrote:
> On Thu 13 Oct 2011 23:42, Linas Vepstas writes:
>
>> In the code that I work on, in (func a b), its rarely the case that a
>> and b are merely strings or lists; they're usually some fairly complex
>> structure, where e.g. 'b' is a list where car and c
On 13 October 2011 20:07, Ian Price wrote:
> Linas Vepstas writes:
>
>> I have no clue why it never occurred to me to use the above paradigm,
>> I will definitely start experimenting with it.
>>
>> Any clue on how to indicate that func returns type 'X' ?
>>
>> I don't know if you were trying to m
On 14 Oct 2011, at 11:28, Ludovic Courtès wrote:
>>> Did you know that Coq would only compile a function when it can prove
>>> that it terminates? That’s another kind of compiler-supported proof one
>>> quickly gets used to.
>>
>> Termination is a non-deducable property. They look at a intuition
Could add some tiny fire drops to this flame, I'd say that
the readability and error-proneness of scheme programs
really depends on what you're doing (and on how you're
doing it)
I don't have any experience with any industrial application
of scheme and I am using it only for the purpose of fun
and
> Did you know that Coq would only compile a function when it can prove
> that it terminates? That???s another kind of compiler-supported proof one
> quickly gets used to.
It's funny how researchers are concerned by proofs that a program
terminates, while most engineers try hard everyday to desig
Hans Aberg skribis:
> On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:
>
>> Did you know that Coq would only compile a function when it can prove
>> that it terminates? That’s another kind of compiler-supported proof one
>> quickly gets used to.
>
> Termination is a non-deducable property. They
Hi,
On Thu 13 Oct 2011 21:39, Tobias Gerdin writes:
> When an error occurs and you are running under the REPL you are
> dropped into the debugger ("Entering a new prompt. .."). This is
> useful. But I am wondering if it is not possible to abort this prompt
> with a user-defined value? That is, t
On Fri 14 Oct 2011 03:07, Ian Price writes:
> Just because scheme doesn't have type declarations doesn't mean you
> can't add them. I often write code that looks like
>
> ; partition : (A -> Boolean) Listof(A) -> Listof(A) Listof(A)
> (define (partition pred list) ...)
I can't find the source ri
On Thu 13 Oct 2011 23:42, Linas Vepstas writes:
> In the code that I work on, in (func a b), its rarely the case that a
> and b are merely strings or lists; they're usually some fairly complex
> structure, where e.g. 'b' is a list where car and cadr must be
> strings, and caddr may or may not be
12 matches
Mail list logo
