Commits

Show all
Author Commit Message Labels Comments Date
Paweł Wieczorek avatarPaweł Wieczorek
universe almost works
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Universe of small types almost works
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Pi-types are small
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Almost all small types are supported
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Empty and Unit types are now small types
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
FundamentalTheorem supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
ConvertibleToReification supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Added NeUniv for ConvertibleToReification
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
ConvertibleToReification supports Universe [without NE]
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Strengthened relation for Univ
Branches
universe_dirty_subset_stronger_rel
Paweł Wieczorek avatarPaweł Wieczorek
adding univ to LR.CTR, failed
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LR.ConvertibleToReification.Fun supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LogReltions.Lift supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Syntax.LogRelTmSyntaxStuff supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Adding Lift
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LogicalRelations.ContextConversion supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LogicalRelations.ProofIrrelevance supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LogicalRelations.ClosedUnderPer supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
LogicalRelations.ClosedUnderConversion supports Univ
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Definition of Logical Relations aligned to Universe; LogicalRelations.Inversion supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Aligned to new version of universe in the model
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
universe dirty subset
Branches
universe_dirty_subset
Paweł Wieczorek avatarPaweł Wieczorek
Removed old NAT_F, added Univ to logical relation
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Almost working SoJ
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
SoundnessOfJudgements - Fun typ related cases work
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Aligning SOJ for universe
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Characterization of PerType works
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Characterization of PerUniv works
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Interp_fun -> InterpType_fun
Branches
universe_bigstep
Paweł Wieczorek avatarPaweł Wieczorek
Interp for PerType works with PerUniv with dependent products
Branches
universe_bigstep
  1. Prev
  2. Next
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.