Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • Max
  • cherry-pick-3bdb2d65
  • computation
  • corinna
  • devel
  • esslli2019
  • master default protected
  • miko4
  • mmtextensions
  • sandboxedMizarImporter
  • stex4
  • tetrapod
  • tptp-exporter
  • undefined
  • v18.0.0
15 results
Created with Raphaël 2.2.028Mar228Feb272620Dec193Sep30Aug20Jun1831May24Apr2221138331Mar2621201511106421Feb4Jan21Dec16Oct27Sep201918131211Aug31Jul271714131211107328May1222Apr2120191815141321Mar1817151098765128Feb272618161514131110987654322Jan211927Dec30Nov1718Oct1714926Sep15138723Aug15929Jul252118117654230Jun2928232221201917131110982131May3029282726252423221614131211532129Apr272322201615121110875432131Mar3028272524232221181714112112Jan6Dec29Nov2521119830Oct292823222112730Sep2820131265330Aug292310927Jul16141312108130Jun24222120181398431May27262017876329Apr27262423221615no messagedeveldeveludate cade-2025 foldermastermasterno messageMerge branch 'master' of mathhub:MMT/LATIN2add Hol TPTP example for DHOL extension paperno messageno messageno messagesoft-typed FOLCorrected and changed Field example.Added Folder for Soft Type Experiments.Changed equivalence relation formalization to just definitions and dependent refinement types. Changed the rest accordingly. Changes were to do refine_I, so streamlined.Corrected quoed_codomain and refined_codomain statements to properly allow a predicate/bin. relation for every B x, instead just a single one. (Surprisingly, identical proofs work.)no messageno messageno messageAdded dhol casestudy: equivalence relations as refinement types.Removed unnecessary stuff from dhol generalized quotient.Changed derivation of repeated quotient to pointwise check. Next: Documentation and chopping down into theories. Need to fix normal DHOL w/ subtypes on-the-fly.Merge branch 'devel' of gl.mathhub.info:MMT/LATIN2 into develGeneralized quotient initial commit.fixing the dependencies in the MANIFEST.MFmiko4 stex4miko4 stex4no neew changesno messageLittle bit cleaned upFormalized all normalization statements, no well-formedness statements.Merge branch 'devel' of gl.mathhub.info:MMT/LATIN2 into develDHOL formalization progress. Half of quotient rules derived.no messagejust added some stuffProved some things.arraysadded basic eqadded concat in sigleton listresolved merge conflictno messageMerge branch 'devel' of gl.mathhub.info:MMT/LATIN2 into develnothing much hereno messageno message