Skip to content
This repository was archived by the owner on May 20, 2018. It is now read-only.

[WIP] Datatype descriptions #172

Open
wants to merge 78 commits into
base: master
Choose a base branch
from
Open

[WIP] Datatype descriptions #172

wants to merge 78 commits into from

Conversation

@robrix
Copy link

@robrix robrix commented Dec 13, 2015

  • Adds a Datatype module containing a Datatype datatype encoded using the other Datatype datatype.
  • Fixes Levitate type descriptions #65.
  • μ.
  • Datatype I must be of type Type₁ rather than Type. Out of scope for this PR.
  • init.
  • ind?
  • Generic constructor (inj).
  • Generic eliminator (elim).

See also:

Rob Rix added 30 commits December 12, 2015 19:25
Stub in a module of datatypes.
bdd775a
Datatype has a Datatype named Datatype.
9faf9c4
Add an end constructor.
1b9853a
Datatype is parameterized by an index type.
41b6e6d
Add a recursive case to Datatype.
4581153
Add an argument case to Datatype.
ff5228c
Add the Datatype module to the directory.
6c26495
Expand the error messages for the encoded Either tests.
29e526a
Stub in a private datatype-encoded boolean module.
bca25eb
Test the equivalence of the datatype-encoded boolean module’s definit…
bc442ee 
…ions with those in the canonical module.
Pull the Datatype declaration into a temporary.
75031d9
Define everything in the datatype-encoded Boolean module.
744f3a6 
This is approximately correct, but note that I’m basically shrugging
when it comes to `BooleanE`, and most of the dependencies aren’t
actually defined.
Merge branch 'master' into datatype-descriptions
302b8d7
Stub in a Tag module.
4c15906
Add the tag module to the directory.
cbf1f67
Tag depends on List.
dadb2f6
Tag depends on String.
603450b
Add an Enum type to the Tag module.
424fb14
The Datatype module depends on the Tag module.
a0affd6
Correct one of the stubbed in terms.
46f799f
Define the Boolean enumeration.
994d78c
Add a Tag binding.
59c6443
Tags eliminate from their specific labels.
5ffd5be
Add a here binding.
447cc08
Eliminate Tag casewise.
a58bcbb
Rename the label parameter.
e37342c
Add a there binding.
67a28f5
The false tag follows the true tag.
e14213c
Log the error messages more legibly.
aac26a7
Log whether this is a type mismatch or a term mismatch.
474ee0e
Rob Rix added 22 commits December 20, 2015 22:50
El expects a type parameter.
5bbcac4
μ expects a type parameter.
7d85abc
Test whether bindings are definitionally equal.
d09ee51
Remove a use of IType.
354e939
Revert "Remove a use of IType."
aef38ef 
This reverts commit 354e939.
Use IType a bit more widely.
cf4ddca
Remove unnecessary parens.
18ab314
Stub in some more of the definition of init.
933cfde
Typecheck the datatype-encoded booleans.
61e9337
Inline the enumeration of boolean case names.
e97a3ba
µ → μ.
0727b6f
Stub in a Branches binding.
f3cd0ff
here/there expect more parameters.
9350cb8
The first argument apparently needs to be List String instead of `E…
0fa4711 
…num`.

Something will need to be done about synonyms not working, but for now
this works around it.
Stub in a case definition.
8ecda22
Type the first argument to case as List String.
a31a773
Stub in the value for case.
ba11f55
Reduce the annotation.
1aa1459 
This seems broken.
Spacing.
8b7dabd
Type the enumerations as Enum.
63aff41
Correct the definitions of first & second.
edee946
Attempt to elaborate the types of applications against a lambda type.
33751b4
@robrix robrix mentioned this pull request Dec 25, 2015
Open
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@robrix