Skip to content

Commit

Permalink
updated readme to remove some ambiguous and incorrect text point out …
Browse files Browse the repository at this point in the history
…by a reviewer. cross referenced with Carlo to try to make sure I got it right this time.
ivoysey committed Nov 2, 2016
1 parent 48633e0 commit a74be66
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
@@ -210,16 +210,16 @@ Assumptions and Representation Decisions
obfuscating the proof text.

One concern with this representation is whether or not it's really
constructive: there are some theorems about contexts that are only about
this representation if you have function extensionality, which amounts to
the Axiom of Choice.
constructive: there are some theorems about contexts that are only
provably about this representation if you have function extensionality,
which is independent from the logic of Agda.

In this case, however, the functions that we build as contexts always
have a finite domain and codomain, so that concern is not as bad as it
might be. That fact is not reflected in the type of contexts. It could be
made explicit by using mappings from `Fin n → τ̇` or paired with a
maximum-name-used-so-far. We have not needed to do that yet, but it is an
easy refactoring if we do in the future.
have a finite domain and codomain. Function extensionality is provable
under that restriction, but the restriction is not reflected in the type
of contexts. It could be made explicit by using mappings from `Fin n → τ̇`
or paired with a maximum-name-used-so-far. We have not needed to do that
yet, but it is an easy refactoring if we do in the future.

- The notion of consistency that we inherit from the work on gradual typing
is deliberately not transitive, so it can't be gracefully encoded with

0 comments on commit a74be66

Please sign in to comment.