| given (p || ~p) | |
| prove (~~p -> p) | |
| proof :: (p + (p -> 0)) -> (((p -> 0) -> 0) -> p) | |
| proof p_or_p0 p0_0 = | |
| case p_or_p0 | |
| Left p => | |
| p | |
| Right p0 => |
| #lang racket | |
| ; This code is in service of @countvajhula's Rhombus equality RRFI at | |
| ; https://github.com/countvajhula/rhombus-prototype/tree/master/rrfi | |
| ; and parts of it should probably be copied into the proof of concept in that | |
| ; repo. | |
| (require racket/generic) | |
| (require rackunit) |
| #lang racket/base | |
| (require (only-in racket/control reset shift)) | |
| (require (only-in racket/match match match-let*)) | |
| (define (my-set! pointer value) | |
| (shift k | |
| `(my-set! ,pointer ,value ,k))) |
| #lang racket | |
| (require rackunit) | |
| ; Hygiene for a curried macro | |
| ; I've been experimenting with a custom system of managed local | |
| ; variables, and I came up with a hygiene test case that was failing. | |
| ; So then I tried the same test case with plain Racket variables, and | |
| ; it failed that way too. Here's a minimalistic example. |
I find compound unquoted expressions to be pretty good for the readability of a code generator. I think this is a good example (from the current version of html-render.rkt):
`(div ([class ,(if top?
"tocviewlist tocviewlisttopspace"
"tocviewlist")])
,(if top? `(div ([class "tocviewtitle"]) ,header) header)
,(if (null? children)
""
`(div ([class ,(cond
| #lang racket/base | |
| (require racket/contract/base) | |
| (provide | |
| (contract-out | |
| [in-merge-sorted (-> (-> any/c any/c boolean?) stream? stream?)])) | |
| (require racket/match | |
| racket/promise |
| #lang racket/base | |
| (require racket/contract/base) | |
| (provide | |
| (contract-out | |
| [in-merge-sorted (-> (-> any/c any/c boolean?) stream? stream?)])) | |
| (require racket/match | |
| racket/promise |
| kick. | |
| that wall. | |
| jump. | |
| and do not fall. | |
| Ice LESS~~ It's the stunt we've gotta do. | |
| To get the fastest SPEEDrun it's what we NEED to train up to. | |
| Up Boomer's tower, practice for seven hours gotta jump, hold | |
| And kick off that loft |
| #lang racket | |
| ; transducers | |
| ; | |
| ; Data structures, algorithms, and utilities for fusable stream | |
| ; manipulations. | |
| ; | |
| ; Inspired by a conversation with Jack Firth, who was using the | |
| ; terminology of "iterators," "collectors," and "transducers," with | |
| ; design goals that involved allowing certain clients to minimizing |
See also the Gist "Cene packages": https://gist.github.com/rocketnia/cac8aa719470f3b6fa4b49e1131270f9
Given a "contribute function" and "contribute argument" based open-world-assumption extension framework, and given the ability to define the same thing more than once if specifying a dex at the same time, it's possible to define transitive closure relations where the entries are contributed as arguments: Contribute a function, have it contribute another function each time it gets an argument, and have that function contribute an argument if the two arguments imply something.
(Rather than just specifying a dex with each definition, we could specify something less general than a merge but more general than a (merge-by-dex ...). Not only would it be idempotent like a merge, but it would also ensure that the result was "backwards compatible" with both inputs -- behaving exactly alike in all non-error cases, and exhibiting no more errors than