Skip to content
This repository has been 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
Contributor

@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:

@robrix
Stub in a module of datatypes.
bdd775a
@robrix
Datatype has a Datatype named Datatype.
9faf9c4
@robrix
Add an end constructor.
1b9853a
@robrix
Datatype is parameterized by an index type.
41b6e6d
@robrix
Add a recursive case to Datatype.
4581153
@robrix
Add an argument case to Datatype.
ff5228c
@robrix
Add the Datatype module to the directory.
6c26495
@robrix
Expand the error messages for the encoded Either tests.
29e526a
@robrix
Stub in a private datatype-encoded boolean module.
bca25eb
@robrix
Test the equivalence of the datatype-encoded boolean module’s definit…
bc442ee 
…ions with those in the canonical module.
@robrix
Pull the Datatype declaration into a temporary.
75031d9
@robrix
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.
@robrix
Merge branch 'master' into datatype-descriptions
302b8d7
@robrix
Stub in a Tag module.
4c15906
@robrix
Add the tag module to the directory.
cbf1f67
@robrix
Tag depends on List.
dadb2f6
@robrix
Tag depends on String.
603450b
@robrix
Add an Enum type to the Tag module.
424fb14
@robrix
The Datatype module depends on the Tag module.
a0affd6
@robrix
Correct one of the stubbed in terms.
46f799f
@robrix
Define the Boolean enumeration.
994d78c
@robrix
Add a Tag binding.
59c6443
@robrix
Tags eliminate from their specific labels.
5ffd5be
@robrix
Add a here binding.
447cc08
@robrix
Eliminate Tag casewise.
a58bcbb
@robrix
Rename the label parameter.
e37342c
@robrix
Add a there binding.
67a28f5
@robrix
The false tag follows the true tag.
e14213c
@robrix
Log the error messages more legibly.
aac26a7
@robrix
Log whether this is a type mismatch or a term mismatch.
474ee0e
@robrix
El expects a type parameter.
5bbcac4
@robrix
μ expects a type parameter.
7d85abc
@robrix
Test whether bindings are definitionally equal.
d09ee51
@robrix
Remove a use of IType.
354e939
@robrix
Revert "Remove a use of IType."
aef38ef 
This reverts commit 354e939.
@robrix
Use IType a bit more widely.
cf4ddca
@robrix
Remove unnecessary parens.
18ab314
@robrix
Stub in some more of the definition of init.
933cfde
@robrix
Typecheck the datatype-encoded booleans.
61e9337
@robrix
Inline the enumeration of boolean case names.
e97a3ba
@robrix
µ → μ.
0727b6f
@robrix
Stub in a Branches binding.
f3cd0ff
@robrix
here/there expect more parameters.
9350cb8
@robrix
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.
@robrix
Stub in a case definition.
8ecda22
@robrix
Type the first argument to case as List String.
a31a773
@robrix
Stub in the value for case.
ba11f55
@robrix
Reduce the annotation.
1aa1459 
This seems broken.
@robrix
Spacing.
8b7dabd
@robrix
Type the enumerations as Enum.
63aff41
@robrix
Correct the definitions of first & second.
edee946
@robrix
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.
1 participant
@robrix