diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-21 00:01:54 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-05-05 18:01:31 -0400 |
| commit | f26f33c1a3916493e7d7e0269a83f6823b7c1419 (patch) | |
| tree | 3ce7b984167833c1bf4d2ec2d2d21f84b5a00321 /src/Experiments/PartialEvaluationWithLetIn.v | |
| parent | d5d68cf089193504746fca948e3c1a706b213e32 (diff) | |
Add notes
Diffstat (limited to 'src/Experiments/PartialEvaluationWithLetIn.v')
| -rw-r--r-- | src/Experiments/PartialEvaluationWithLetIn.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Experiments/PartialEvaluationWithLetIn.v b/src/Experiments/PartialEvaluationWithLetIn.v index ccb2f4585..d6df6db0c 100644 --- a/src/Experiments/PartialEvaluationWithLetIn.v +++ b/src/Experiments/PartialEvaluationWithLetIn.v @@ -1,5 +1,16 @@ Require Import Crypto.Util.Notations. +(** Notes: + +1. pattern out identifiers and types. + - type := arrow (_:type) (_:type) | type_base (_:base_type) -- the latter is a parameter + - literal is an identifier + - expr cases: var, abs, app, letin, ident -- ident is a parameter +2. add prenex polymorphism for identifiers (type variables) + - + - ident is indexed by typecodes, perhaps cases: arrow | base | typevar +*) + Module type. Inductive type := nat | prod (A B : type) | arrow (s d : type). End type. |