Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Jul23Jun221410Feb5432131Jan2928272625242221201817161512987643220Dec19181615141312109826Nov252422211817158124Oct2320191815141211109527Sep25242320174331Aug3015Jul29Jun25May201917Mar1619Feb719Jan16Dec1454130Nov282731Oct30282019119229Sep2524Jul87121Jun20173227May26221817141127Apr2322212017151413129876432130Mar242321171211109543228Feb272624212017231Jan30291613818Nov25Oct24Use implications instead of conjunctionsmastermasterSome documentation on testsUpdate testsFormals encoded as *dependent* telescopesRevert "Try to typecheck real_defs"Make runtest exit with output 1 when test failsFixed telescopesTry to typecheck real_defsupdating CIadd option to only translate preludeMerge branch 'devel'Prepare release 0.1Merge branch 'devel'Add lisp testing for preludeProper test for translatorSome notes, cast functionUpdated translatable theoriesSystematically get the supertype of expr-as-typeUpdate forbidden lettersRe introducing opacitySlightly simpler formal handlingDon't store theory bindingsNo need for *ctx*Improvements over bindingsAllow abstract-over to take single elementsBetter pprint formalsHandle full fledged telescopesDocumentationLisp testingDynamically bind global variables in pp-dkMore lisp for tests, prelude as a testMerge branch 'lp2' into develUpdating proof toolsAdapting json to new typecheckingCI nitpicksExpliciting coercion rulesUse SBCL for common tasksprelude check does not need psnj anymoreMerge branch 'devel' into lp2fix tests