Takafumi Saikawa
Takafumi Saikawa
`changelog.txt` currently lists removed Definitions / Lemmas / etc. but not what to use instead, making the user stuck at upgrading their scripts dependent on the removed things. This draft...
Finished defining ereal_convType, but with very unclean proofs. @affeldt-aist Could you take a glance at the changes?
This is an experiment to switch algebraic operations on random variables to the generic ones on `ringType`. Some lemmas in proba.v, aep.v, typ_seq.v needed rather big modifications, while the proofs...
The definition of qperm function in the quicksort branch requires an interaction between fixpoints and binds to show its termination. Currently there is no such mechanism, and it seems hard...
The branch keimel contains proofs of some significant lemmas. Let us incorporate them into somewhere in the master as soon as one remaining admit is completed.
`Typecore.type_pat` had two modes, one for typing patterns from programs, and another for retyping potential counter-examples generated by `Parmatch`. This mixture of purposes resulted in several complexities: 1. In order...
There is a `ringType` decaration for function types in topology.v, which I have recently found useful for some projects (namely affeldt-aist/infotheo and ieva-itu/robustmean) with no topology. Unfortunately, importing topology conflicts...
This draft PR is an attempt to formalize power series. The goals are * to prove useful convergence tests * to provide arithmetic for power series * to abstract already...
It would be nice to have many exercise-level facts proved in the library, which would support the consistency of our formalization. An example is that every metric space is T4...
This PR introduces wrapper functions for level management (`Ctype.wrap_def`, etc) and for type variable scoping (`Typetexp.wrap_type_variable_scope`). The older API (`Ctype.{begin_def,end_def}`, `Typetexp.{narrow,widen}`, etc.) is removed. The goal is to clarify the...