Max S. New maxsnew
maxsnew
/ Cubical.Foundations.Isomorphism.More.agda
Created
November 27, 2024 17:55
two versions of dependent isomorphisms
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --safe #-} | |
| module Cubical.Foundations.Isomorphism.More where | |
| open import Cubical.Foundations.Prelude | |
| open import Cubical.Foundations.Equiv | |
| open import Cubical.Foundations.Isomorphism | |
| open import Cubical.Data.Sigma | |
| private | |
| variable |
maxsnew
/ GuardedKanren.agda
Last active
September 4, 2024 14:51
— forked from rntz/GuardedKanren.agda
implementation of muKanren's search strategy in Agda with --guarded
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --guarded #-} | |
| module GuardedKanren where | |
| open import Agda.Primitive using (Level; _⊔_) | |
| private variable | |
| l l' : Level | |
| A B : Set l | |
| data Bool : Set where true false : Bool | |
| if_then_else_ : ∀{A : Set} → Bool → A → A → A |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module ChurchList where | |
| open import Cubical.Foundations.Prelude | |
| open import Cubical.Foundations.Isomorphism | |
| import Cubical.Data.List as List | |
| open import Cubical.Data.List using (List) | |
| private | |
| variable ℓ : Level |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Bool.Bool. | |
| Inductive Sexp := | |
| | Atom : bool -> Sexp | |
| | List : Forest -> Sexp | |
| with | |
| Forest := | |
| | Nil : Forest | |
| | Cons : Sexp -> Forest -> Forest. |
maxsnew
/ equi-recursive-success.rkt
Last active
July 25, 2018 20:01
Trying to encode a bidirectional lambda-calculus in Typed Racket with structural types
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #lang typed/racket | |
| (define-type Var String) | |
| (define-type Type (U 'Base (List '-> Type Type))) | |
| (define-type Ctx (Listof (Pair Var Type))) | |
| (define-type Expr (U Var (List 'App Expr Term) (List 'Asc Type Term))) | |
| (define-type Lam (List 'Lam Var Term)) | |
| (define-type Term (U Expr Lam)) | |
| (define-predicate lam? Lam) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def print_upper(s : str): | |
| up_s = s.upper() | |
| def printer(n : int): | |
| acc = "" | |
| for i in range(0,n): | |
| acc += up_s | |
| return acc | |
| return printer |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [mnew:~CODE/racket/Redex-Enum-Paper]$ scribble --latex --dest x paper.scrbl (master) | |
| [Output to x/paper.tex] | |
| Warning: some cross references may be broken due to undefined tags: | |
| (counter ("figure" "fig:benchmark-lines")) | |
| (counter ("figure" "fig:benchmark-lines" "value")) | |
| (counter ("figure" "fig:benchmark-overview")) | |
| (counter ("figure" "fig:benchmark")) | |
| (counter ("figure" "fig:correlation" "value")) | |
| (counter ("figure" "fig:benchmark-overview" "value")) | |
| (counter ("figure" "fig:benchmark" "value")) |
maxsnew
/ lifetime-error-fixed.rs
Last active
August 29, 2015 14:07
Non-deterministic Lifetime Error
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| extern crate graphviz; | |
| use graphviz as dot; | |
| use std::str; | |
| type Nd = uint; | |
| type Ed = (uint, uint); | |
| struct Graph<'a> { | |
| nodes: Vec<&'a str>, | |
| edges: Vec<Ed>, |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| data Request = PutS String | |
| | Exit Int | |
| | GetS | |
| port out : Signal (Maybe Request) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html> | |
| <head> | |
| <title>Test</title> | |
| <script src="resources/elm-runtime.js"></script> | |
| <script src="build/Ports.js"></script> | |
| </head> | |
| <body> | |
| <h1>Test</h1> | |
| <div id="bug"></div> |
NewerOlder