# \#redex

**URL:** https://racket.discourse.group/tag/redex/206.md

[Latest](https://racket.discourse.group/latest.md) · [Categories](https://racket.discourse.group/categories.md) · [Tags](https://racket.discourse.group/tags.md)

---

## [Is there any Redex implementation of a very minimal dependently typed Lambda Calculus core? Something like Elaboration-Zoo-02](https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957)

<div class="topic-metadata">

**Author:** [@B0B](https://racket.discourse.group/u/B0B)\
**Replies:** 1\
**Last updated:** [June 8, 2024, 10:04pm UTC](https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957 "2024-06-08T22:04:48Z")

</div>

I'd like to prototype/play-around-with a dependently typed language. I'm very new to Racket, but would like to use Redex (or any similar tool) to define some decent typing and evaluation rules. I've gone through the tw…

---

## [How to type amb in the redex exercise?](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954)

<div class="topic-metadata">

**Author:** [@benknoble](https://racket.discourse.group/u/benknoble)\
**Replies:** 4\
**Last updated:** [June 6, 2024, 5:18pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954 "2024-06-06T17:18:43Z")

</div>

A long time ago I was looking at Exercise 6 in the Redex tutorial, and I stumbled on to the following: I though it would be straightforward to modify the grammar to accept a type (e.g. , (amb t e ...) or (amb e ... : t) …