cur

cur copied to clipboard

run `ntac/trace` with this example (from here: https://github.com/wilbowma/cur/issues/121) ``` (ntac/trace (∀ (T : Type) (Σ (lst : (List T)) (And (== (List T) lst (nil T)) (Not (== (List T)...

stchang

Printable data types

3

I want support for making numbers print like numbers. I can redefine `#%datum` to get numbers to read like numbers, but want vice versa. Some kind of interface to `gen:printable`?

wilbowma

```racket #lang cur (define-datatype Nat : Type (z : Nat) (s : (-> Nat Nat))) (define-datatype Vec (A : Type) : (-> Nat Type) (nil : (Vec A z)) (cons...

wilbowma

Should have renamed these during the turnstile merge.

wilbowma

Add some solvers!

1

SAT/SMT: https://planet.racket-lang.org/package-source/ianj/smt-solver.plt/1/1/planet-docs/smt-solver/An_SMT-solver_for_Racket.html#(def._((planet._smt-solve..rkt._(ianj._smt-solver..plt._1._0)._smt-solver)._smt-solve)) Systems of equations: https://docs.racket-lang.org/math/matrix_solve.html

wilbowma

M Gordon, R Milner, L Morris, M Newe, C. Wadsworth. 1978

wilbowma

Wouldn't it be nice if we had η-expansion during conversion? Coming soon.

wilbowma

define/rec/match needs another way to specify matching args

1

stchang

Make #lang cur vs #lang cur/base

4

For accessibility, `#lang cur` should probably import most of the things by default, and other `#lang`s can be provided more restricted imports. `#lang cur` should include: - [ ] sugar...

wilbowma

With the Turnstile+ merge, documentation is now in poor shape. For accessibility, this is probably the priority right now.

wilbowma