aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Collapse)AuthorAge
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
| | | | | | | | Now it works not just at top-level, but also in, e.g., arguments to hypotheses. We had to change some proofs because it no longer moves the hypotheses it changes to the bottom.
* Add aborted MapCastByDeBruijnWfGravatar Jason Gross2017-03-19
| | | | | | | | I'm not sure exactly why the wf proof requires cast_backb in map_cast; it seems to be used as a dumb way of instantiating the context-extension on the input expression tree (since we're only given the context-extension values on the output expression, which has a different type).
* Finish MapCastCorrectGravatar Jason Gross2017-03-19
|
* Add more to CompileWfGravatar Jason Gross2017-03-19
|
* Add MapCastWfGravatar Jason Gross2017-03-19
|
* Most of the way towards a complete MapCastCorrectGravatar Jason Gross2017-03-19
|
* Add Named/PositiveContext/DefaultsProperties.vGravatar Jason Gross2017-03-19
|
* Finish CompileInterp proofGravatar Jason Gross2017-03-19
|
* Split up ContextPropertiesGravatar Jason Gross2017-03-19
|
* Add mname_list_unique_nilGravatar Jason Gross2017-03-19
|
* Add more ContextPropertiesGravatar Jason Gross2017-03-19
|
* Add {m,o,}name_list_uniqueGravatar Jason Gross2017-03-19
|
* Add Addmitted correctness for MapCastByDeBruijnGravatar Jason Gross2017-03-19
|
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
| | | | | This will allow us to use the same syntax type for the new version of word-size selection without needing to rip out all of the old things.
* Minor simplification in SmartBoundGravatar Jason Gross2017-03-18
|
* Switch to more robust automation in MapCastInterpGravatar Jason Gross2017-03-17
|
* Add default_names_for{,f}Gravatar Jason Gross2017-03-17
|
* Add IdContextGravatar Jason Gross2017-03-17
|
* Revert "Have cast_op return exprf instead of op"Gravatar Jason Gross2017-03-17
| | | | | | This reverts commit bcfcb5e91011ad0dda68e2b41f871058cf890a3c. Doesn't actually build
* Have cast_op return exprf instead of opGravatar Jason Gross2017-03-17
| | | | cc @andres-erbsen
* Add MapCastByDeBruijn on PHOAS syntaxGravatar Jason Gross2017-03-17
|
* Don't pass a wf proof into InterpToPHOASGravatar Jason Gross2017-03-17
| | | | | Use a fail-value instead. This makes it easier to compose with other transformations.
* Add aborted in-process compile-{wf,interp} proofsGravatar Jason Gross2017-03-17
|
* Add a Named version of MapCastGravatar Jason Gross2017-03-17
| | | | Based on Andres' work towards #123.
* Fix a name clashGravatar Jason Gross2017-03-14
|
* Add split_{m,o,}names_firstn_skipn and co.Gravatar Jason Gross2017-03-14
|
* Add NameUtilPropertiesGravatar Jason Gross2017-03-14
|
* Add InterpretToPHOASInterpGravatar Jason Gross2017-03-14
|
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
|
* Remove useless hypsGravatar Jason Gross2017-03-14
|
* Add InterpretToPHOASGravatar Jason Gross2017-03-14
|
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
|
* Add ContextPropertiesGravatar Jason Gross2017-03-14
|
* Remove useless importsGravatar Jason Gross2017-03-14
|
* Move ContextOk to ContextDefinitionsGravatar Jason Gross2017-03-14
|
* Add lemma about wff and interpf of NamedGravatar Jason Gross2017-03-14
|
* Fix more unfoldingGravatar Jason Gross2017-03-10
|
* Fix more unfolding that shouldn't happenGravatar Jason Gross2017-03-10
|
* Make sure interp_flat_type isn't unfolded in SmartMapGravatar Jason Gross2017-03-10
|
* Add better SmartFlatTypeMapInterp2Gravatar Jason Gross2017-03-08
|
* Remove interp_genf from Named/SyntaxGravatar Jason Gross2017-03-08
|
* Remove stuff from Reflection/Named/SyntaxGravatar Jason Gross2017-03-08
|
* Add FMapContext, PositiveContextGravatar Jason Gross2017-03-08
| | | | | Also copy some definitions from Syntax out of it, in prep for removing them
* make 8.5 happyGravatar Andres Erbsen2017-03-02
|
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
|
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
|
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
| | | | | | | | | | | This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
* Add interp_flat_type_rel_pointwise_SmartVarfMap, ↵Gravatar Jason Gross2017-02-28
| | | | interp_flat_type_rel_pointwise_Reflexive
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
|
* Deduplicate codeGravatar Jason Gross2017-02-28
| | | | There was duplicate code in Reflection.Equality and Reflection.TypeInversion
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-15 09:58:05 +0000