1. Paweł Wieczorek
  2. MgrCoq

Commits

Show all
Author Commit Message Date Builds
Paweł Wieczorek
merge with branch, universe is supported
Paweł Wieczorek
cleaning
Paweł Wieczorek
Univ finished
Paweł Wieczorek
universe almost works
Paweł Wieczorek
Universe of small types almost works
Paweł Wieczorek
Pi-types are small
Paweł Wieczorek
Almost all small types are supported
Paweł Wieczorek
Empty and Unit types are now small types
Paweł Wieczorek
FundamentalTheorem supports Universe
Paweł Wieczorek
ConvertibleToReification supports Universe
Paweł Wieczorek
Added NeUniv for ConvertibleToReification
Paweł Wieczorek
ConvertibleToReification supports Universe [without NE]
Paweł Wieczorek
adding univ to LR.CTR, failed
Paweł Wieczorek
LR.ConvertibleToReification.Fun supports Universe
Paweł Wieczorek
LogReltions.Lift supports Universe
Paweł Wieczorek
Syntax.LogRelTmSyntaxStuff supports Universe
Paweł Wieczorek
Adding Lift
Paweł Wieczorek
LogicalRelations.ContextConversion supports Universe
Paweł Wieczorek
LogicalRelations.ProofIrrelevance supports Universe
Paweł Wieczorek
LogicalRelations.ClosedUnderPer supports Universe
Paweł Wieczorek
LogicalRelations.ClosedUnderConversion supports Univ
Paweł Wieczorek
Definition of Logical Relations aligned to Universe; LogicalRelations.Inversion supports Universe
Paweł Wieczorek
Aligned to new version of universe in the model
Paweł Wieczorek
universe dirty subset
Paweł Wieczorek
Removed old NAT_F, added Univ to logical relation
Branches
universe_bigstep
Paweł Wieczorek
Almost working SoJ
Branches
universe_bigstep
Paweł Wieczorek
SoundnessOfJudgements - Fun typ related cases work
Branches
universe_bigstep
Paweł Wieczorek
Aligning SOJ for universe
Branches
universe_bigstep
Paweł Wieczorek
Characterization of PerType works
Branches
universe_bigstep
Paweł Wieczorek
Characterization of PerUniv works
Branches
universe_bigstep
  1. Prev
  2. Next