on bc8da8d help sign in
all commits
a750910Merge pull request #3795 from kaeluka/patch-1Ahmad Salim Al-Sibahi 31def51Mention do-notation in elab shell docsAlex Gryzlov 8c3ecb8Docs: ``ElabReflection`` needs explicit enablingStephan Brandauer 0df1270Change Instance to implementation (#3404)(λ _ λ) 1726bf9Changed type classes in error messages and documentation to interfaces where necessary (previously forgotten)Ahmad Salim Al-Sibahi 291ccdcJust/Nothing for intro was split into intro/intro'Chris Allen eeb1384debuggging --> debuggingOzgur Akgun d75e4c6Remove advice to import Language.Reflection.ElabJeremy W. Sherman c6c4bf4Drop claim that general-purpose commands are general REPL commandsJeremy W. Sherman d17f246Remove duplicated phraseJeremy W. Sherman f30db6bFix typo: reply -> REPLJeremy W. Sherman 6a7b071Update the list of elaboration shell commandsJeremy W. Sherman be11838Removes :q alias for :abandonJeremy W. Sherman c18bf77Rephrases section "Interactively building elaboration scripts"Jeremy W. Sherman 002e9b9elaborator-reflection.rst: Fix rendering of bulleted listJeremy W. Sherman 8a1bc7dUpdate tactics documentation based on deprecationDavid Raymond Christiansen a0d8376Merge pull request #2518 from jeremy-w/jeremy-w/mark-interactive-proving-as-deprecatedNiklas Larsson 7f6f3c4Spelling in Sphinx documentationEcho Nolan 90b7d07Point readers at Elaborator ReflectionJeremy W. Sherman 62bb361Merge pull request #2408 from mjgpy3/metavariable_to_hole_docsDavid Christiansen 696f336Replace "metavariable" with "hole"Michael Gilliland 6923b54Fixed reST usage in elaborator reference.Jan de Muijnck-Hughes 54cd5a6An interactive Elab shellDavid Raymond Christiansen 5db2080Initial elab reflection docsDavid Raymond Christiansen bfa72a9Initial docs for %runElabDavid Raymond Christiansen