These are extracted from discussions I triggered on the Racket Slack. Thanks to everyone who participated in the discussion threads! :-)
Use (and value #t)
to convert a value to its boolean equivalent.
#lang racket/gui | |
(require plot | |
pict) | |
;;; Author: Laurent Orseau | |
;;; License: [Apache License, Version 2.0](http://www.apache.org/licenses/LICENSE-2.0) or | |
;;; [MIT license](http://opensource.org/licenses/MIT) at your option. | |
;;; See in particular this blog bost: | |
;;; https://alex-hhh.github.io/2019/09/map-snip.html#2019-09-08-map-snip-footnote-2-return |
[ | |
{ | |
"key": "ctrl+shift+tab", | |
"command": "workbench.action.previousEditor" | |
}, | |
{ | |
"key": "ctrl+tab", | |
"command": "workbench.action.nextEditor" | |
} | |
] |
{-# OPTIONS --safe #-} | |
module ULCOmega where | |
open import Data.Nat.Base using (ℕ ; zero ; suc) | |
open import Data.Fin.Base as Fin using (Fin) | |
import Data.Nat.Literals | |
import Data.Fin.Literals | |
open import Data.Unit using (⊤ ; tt) -- for instance resolution |
{-# OPTIONS --without-K --safe #-} | |
module TwistedMaxAcc where | |
open import Data.Nat using (ℕ ; zero ; suc ; _>_ ; _≤_ ; _≤″_ ; less-than-or-equal ; _≰_ ; _>?_ ; _≤?_ ; _+_) | |
open import Data.Nat.Properties using (≤-reflexive ; ≤-antisym ; ≮⇒≥ ; >⇒≢ ; ≤⇒≤″ ; m≤m+n ; +-suc ; +-comm) | |
open import Data.Empty using (⊥-elim ; ⊥) | |
open import Relation.Nullary using (Dec ; yes ; no) | |
open import Relation.Binary.PropositionalEquality.Core using (refl ; _≡_ ; subst ; sym) |
#| | |
building syntax objects | |
cpu time: 106 real time: 112 gc time: 45 | |
expanding | |
cpu time: 16063 real time: 17360 gc time: 2152 | |
building syntax objects 2 | |
cpu time: 116 real time: 126 gc time: 50 | |
expanding | |
cpu time: 15898 real time: 16583 gc time: 2231 |
{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs. | |
Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -} | |
open import Data.Empty using (⊥) | |
open import Data.Unit using (⊤; tt) | |
open import Data.Nat using (ℕ; zero; suc) | |
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax) | |
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) | |
infix 3 _-→_ _-↛_ |
{-# OPTIONS --without-K --safe #-} | |
{- Works with Agda 2.6.2 -} | |
module InstMagic where | |
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl) | |
open import Data.List using (List ; [] ; _∷_) | |
open import Data.Unit using (⊤ ; tt) | |
open import Data.Nat using (ℕ ; zero ; suc ; _≟_) | |
open import Data.List.Relation.Unary.Any using (Any ; any? ; here ; there) |
#lang racket/base | |
(require racket/list | |
racket/match | |
racket/class | |
racket/pretty | |
racket/snip | |
racket/gui/base | |
framework) |
#lang racket/base | |
(require (for-syntax racket/base | |
syntax/parse) | |
racket/stxparam) | |
;; (bind x-id e-expr) | |
;; Bind x-id to some string in e-expr | |
;; Expands to a expression that constructs a hash | |
;; table storing e-expr in a field |