e
>
> Disassembling around the failed instruction address (with `disassemble`
> in gdb) should clarify what instruction is misused.
>
> Thanks,
> Matthew
>
> At Tue, 11 Aug 2020 10:58:03 -0700 (PDT), Joey Eremondi wrote:
> > I'm wondering, does anybody have any prebu
I'm wondering, does anybody have any prebuilt 32-but ARM binaries for
Racket on Chez? I'm trying to run a little web-server on a raspberry pi,
and I'd prefer to use the Chez version, but I can't seem to get it to build.
Alternately, if anybody knows why it won't build and can help, that would
:30 -0800 (PST), Joey Eremondi wrote:
> > I'm using Scribble and Frog to automatically generate a publications
> list
> > from a BibTex file. The problem is, right now I get the same order
> > regardless of what order I call ~cite: sorted by year, oldest to newest.
I'm using Scribble and Frog to automatically generate a publications list
from a BibTex file. The problem is, right now I get the same order
regardless of what order I call ~cite: sorted by year, oldest to newest.
I'd like the reverse of this, with newest at the top. Is it possible to
change
I'm wondering, are there any good examples out there of using #:inv with
Redex-judgments? Particularly with asserting that some other judgment holds
on the output.
For example, I've got:
#:contract (SomeJudgment Gamma tt gv gU)
#:inv ,(judgment-holds (SomeOtherJudgment gv gU))
The problem
As part of my ongoing attempt to turn my Redex model into a #lang, I'm
wondering, is there a way to fully expand and evaluate a syntax object at
compile-time? I'm trying to get compile-time typechecking working.
Here's what I have:
* My Redex model uses names like TermLam, TermApp etc.
*
I'm modelling dependent types in redex, and I've got a rule that looks like
this:
[
(WellFormed (EnvExt x gU Gamma))
(Check (EnvExt x gU Gamma) gu gV)
---
"CheckLamPi"
(Check Gamma (CanonicalLam x gu) (CanonicalPi x gU
nt forms too.
>
> Robby
>
> On Wed, Jan 2, 2019 at 9:18 PM Joey Eremondi > wrote:
> >
> > I'm wondering, is there a way to show some sort of trace for a call to
> judgment-holds that returns '() or #f?
> >
> > I'm in a situation where a judgment that I e
I'm wondering, is there a way to show some sort of trace for a call to
judgment-holds that returns '() or #f?
I'm in a situation where a judgment that I expect to hold does not, and
it's tricky to find out by hand where it is failing. The #mode requirement
for the judgments suggests an obvious
Thanks for the response!
That's not quite what I want. That will quote lambdas and applications into
my redex models, but I also want it to reduce them by my reduction relation.
The link I posted discussed how to do that, but only when you write
programs in the syntax of the model.
Sorry for
I've got a model for a language I'm working on in PLT Redex, but it's
auto-generated by another tool (Ott). Because of this, the syntax comes out
in somewhat obfuscated format:
(define-language L
(term ::= (TermLambda var term)
var
(TermApp term term) )
I've found
11 matches
Mail list logo
