PasteRack.org
Paste #
10452
2021-02-02 12:32:18
Fork
as a new paste.
Paste viewed 350 times.
Tweet
Embed:
<link type="text/css" rel="stylesheet" href="http://pasterack.org/scribble.css"/><link type="text/css" rel="stylesheet" href="http://pasterack.org/racket.css"/><link type="text/css" rel="stylesheet" href="http://fonts.googleapis.com/css?family=Droid+Sans+Mono"/><div style="font-family:'Droid Sans Mono',monospace;background-color:transparent"><ol start="0" style="font-size:70%;color:#A0A0A0"><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><a class="RktModLink" data-pltdoc="x" href="http://docs.racket-lang.org/guide/Module_Syntax.html#%28part._hash-lang%29"><span class="RktMod">#lang</span></a><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><a class="RktModLink" data-pltdoc="x" href="http://docs.racket-lang.org/reference/index.html"><span class="RktSym">racket</span></a><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"> </span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._require%29%29">require</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">redex</span><span class="RktPn">)</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._require%29%29">require</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym"><a class="RktValLink" data-pltdoc="x" href="http://docs.racket-lang.org/pict/Pict_Datatype.html#%28def._%28%28lib._pict%2Fmain..rkt%29._pict%29%29">pict</a></span><span class="RktPn">)</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"> </span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-language%29%29">define-language</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">L</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym">A</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">number</span><span class="RktPn">)</span><span class="RktPn">)</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"> </span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-metafunction%29%29">define-metafunction</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">L</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">fn</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">:</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">A</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/reference/function-contracts.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._-~3e%29%29"><span class="nobreak">-></span></a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">A</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktPn">[</span><span class="RktPn">(</span><span class="RktSym">fn</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">A</span><span class="RktPn">)</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">A</span><span class="RktPn">]</span><span class="RktPn">)</span><span class="RktMeta"></span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"> </span></span></li><li><span style="font-family:'Droid Sans Mono',monospace;font-size:125%"><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktValLink" data-pltdoc="x" href="http://docs.racket-lang.org/pict/Pict_Datatype.html#%28def._%28%28lib._pict%2Fmain..rkt%29._pict-descent%29%29">pict-descent</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktPn">(</span><span class="RktSym"><a class="RktStxLink" data-pltdoc="x" href="http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._metafunction-~3epict%29%29">metafunction->pict</a></span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktSym">fn</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktPn">#:contract?</span><span class="RktMeta"></span><span class="hspace"> </span><span class="RktMeta"></span><span class="RktVal">#t</span><span class="RktPn">)</span><span class="RktPn">)</span><span class="RktMeta"></span></span></li></ol><p>=></p><div><pre></pre></div></div>
#lang
racket
(
require
redex
)
(
require
pict
)
(
define-language
L
(
A
number
)
)
(
define-metafunction
L
fn
:
A
->
A
[
(
fn
A
)
A
]
)
(
pict-descent
(
metafunction->pict
fn
#:contract?
#t
)
)
=>