diff --git a/README.md b/README.md new file mode 100644 index 0000000..7b841ad --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +cur +=== + +CIC under Racket. A language with static dependent-types and dynamic +types, type annotations and parenthesis, theorem proving and +meta-programming. + +> Noun +> cur (plural curs) +> > 1. (archaic) A mongrel or inferior dog. +> > 2. (archaic) A detestable person. diff --git a/coq-extraction.rkt b/coq-extraction.rkt index ef0c78a..1e20712 100644 --- a/coq-extraction.rkt +++ b/coq-extraction.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" (begin-for-syntax (define orig-insp (variable-reference->module-declaration-inspector diff --git a/redex-core.rkt b/cur-redex.rkt similarity index 100% rename from redex-core.rkt rename to cur-redex.rkt diff --git a/example.rkt b/example.rkt index f03a1dc..c275f3a 100644 --- a/example.rkt +++ b/example.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" ;; Use racket libraries over your dependently typed code!?!? ;; TODO: actually, I'm not sure this should work quite as well as it diff --git a/nat.rkt b/nat.rkt index 09da5ea..c1bc774 100644 --- a/nat.rkt +++ b/nat.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" (require "sugar.rkt") (data nat : Type diff --git a/pltools.rkt b/pltools.rkt index 32b88f7..ae5b44c 100644 --- a/pltools.rkt +++ b/pltools.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" (require "sugar.rkt" "nat.rkt") ;; TODO: Can't export var, avar because technically these aren't ;; defined.... diff --git a/proofs-for-free-v2.rkt b/proofs-for-free-v2.rkt index bae25f9..604bcea 100644 --- a/proofs-for-free-v2.rkt +++ b/proofs-for-free-v2.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" (require rackunit racket/trace (for-syntax racket/syntax)) ;; TODO: Move to standard library diff --git a/sugar.rkt b/sugar.rkt index 021b77e..b280f1d 100644 --- a/sugar.rkt +++ b/sugar.rkt @@ -1,4 +1,4 @@ -#lang s-exp "redex-core.rkt" +#lang s-exp "cur-redex.rkt" (provide -> ->* forall*