diff --git a/doc/applications/index.md b/doc/applications/index.md index f6a4110..7435c7d 100644 --- a/doc/applications/index.md +++ b/doc/applications/index.md @@ -18,7 +18,7 @@ In particular, these include The [MMT API](../api) based on MMT provides a number of knowledge management services including * notation-based presentation, -* interactive web-browisng, +* interactive web-browsing, * MMT-aware databases with custom indexing and retrieval, * project-based abstraction and work flows for building, distribution, and sharing, * management of change, diff --git a/doc/applications/intellij/index.md b/doc/applications/intellij/index.md index e183591..ad39f5f 100644 --- a/doc/applications/intellij/index.md +++ b/doc/applications/intellij/index.md @@ -3,7 +3,7 @@ layout: doc title: IntelliJ-MMT Plugin --- -[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sourecs. It serves the usual features of "language plugins": +[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sources. It serves the usual features of "language plugins": - syntax highlighting - type checking diff --git a/doc/applications/intellij/installation.md b/doc/applications/intellij/installation.md index b615a7c..e9c7af5 100644 --- a/doc/applications/intellij/installation.md +++ b/doc/applications/intellij/installation.md @@ -48,5 +48,5 @@ Since MMT files make heavy use of Unicode math charcters, be sure to have a font ### Notes on automatic type checking -- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenvient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT) +- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT) - The *Document Tree* (on the left border of the IntelliJ-Window) only shows the syntax tree of the document that has been type checked last. To see the tree for the currently opened document, check the *Type Checking* checkbox in the *Errors* panel. Automatically navigating the syntax tree by caret position in the document can be turned on and off with the corresponding check box at the top of the *Document Tree* panel. diff --git a/doc/applications/jedit.md b/doc/applications/jedit.md index 8628c9f..4410eed 100644 --- a/doc/applications/jedit.md +++ b/doc/applications/jedit.md @@ -52,7 +52,7 @@ This turns the system into a (very simple) interactive theorem prover. The type checker treats any occurrence of _ in MMT terms as a fresh unknown and tries to infer its value. This includes calling the (experimental and very weak) automated theorem prover of MMT. -If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the soruce. +If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the source. If the prove fails but the expected type of the subterm is found, a hole-term is introduced. In the latter case, the command introduce-hole can be used to replace _ with the hole-term in the source (e.g., in order to use auto-completion). diff --git a/doc/applications/server.md b/doc/applications/server.md index 2028563..50f82cb 100644 --- a/doc/applications/server.md +++ b/doc/applications/server.md @@ -52,7 +52,7 @@ Some features are: * a *symbol* shows its full MMT URI as a tooltip. * a *variable* selects its declaration. * The *right-click menu* permits setting visibility options for the selected subexpression. - These show/hide parts of the expression that were infered by the system: + These show/hide parts of the expression that were inferred by the system: * *reconstructed types*: the omitted types of bound variables * *implicit arguments*: the omitted arguments to operator applications * *redundant brackets*: brackets that are not needed due to operator precedences diff --git a/doc/applications/shell.md b/doc/applications/shell.md index e91b9f3..01bac86 100644 --- a/doc/applications/shell.md +++ b/doc/applications/shell.md @@ -12,7 +12,7 @@ Each subclass comes with scaladoc and can be best understood by browsing the kno The up-to-date context-free grammar for shell commands is part of the constructor parser in the companion object `Action` and can be best understood by reading the source code. ### ANSI Formatting in the MMT Shell -Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formating, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively. +Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formatting, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively. ### MMT Scripts An MMT script is a text file containing one shell command per line. (Empty lines are allowed, lines starting with // are ignored.) diff --git a/doc/applications/tgview.md b/doc/applications/tgview.md index 8eb2a1e..cfc29ff 100644 --- a/doc/applications/tgview.md +++ b/doc/applications/tgview.md @@ -2,7 +2,7 @@ layout: doc title: TGView (the MMT Theory Graph viewer) --- -TGView is a brower-based theory graph viewer based on the [VisJS](http://visjs.org/) +TGView is a browser-based theory graph viewer based on the [VisJS](http://visjs.org/) network library. The code is [available on GitHub](https://github.com/UniFormal/TGView), and a [MathHub instance](http://mmt.mathhub.info/graphs/tgview) gives visual access to the MathHub archives as interactive theory graphs. diff --git a/doc/archives/Mathhub/lmh.md b/doc/archives/Mathhub/lmh.md index f37f8ee..6ea1795 100644 --- a/doc/archives/Mathhub/lmh.md +++ b/doc/archives/Mathhub/lmh.md @@ -35,7 +35,7 @@ LMH also allows installing a specific branch of an archive. The syntax for this lmh install @ -Archvies are versioned using git. +Archives are versioned using git. A version of an archive can be a branch name or a git commit hash (Technically anything that is a ref in git). When a non-existing version of the archive is specified, lmh will display a warning message and then fall back to the default version. If `lmh install` with a specific version is called on an archive that is already installed, it will make sure to update to the specified version. diff --git a/doc/archives/building.md b/doc/archives/building.md index 86ac99d..693b1fa 100644 --- a/doc/archives/building.md +++ b/doc/archives/building.md @@ -10,7 +10,7 @@ MMT can be used as a build tool using a special [shell command](../applications/ ### Defining Build Targets The collection of build targets is maintained by the [extension manager](../api/extensions/). New build targets are defined by implementing the [`archives.BuildTarget`](apidoc://info.kwarc.mmt.api.archives.BuildTarget) class. -Build target modfiers and change management are supported for automatically for every build target. +Build target modifiers and change management are supported for automatically for every build target. ### Build Target Modifiers diff --git a/doc/archives/meta_inf.md b/doc/archives/meta_inf.md index a54592e..e4b6b7c 100644 --- a/doc/archives/meta_inf.md +++ b/doc/archives/meta_inf.md @@ -20,5 +20,5 @@ narration-base | the URI prefix prepended to the file paths inside the archives source, content, narration, relational | custom folder names for specific dimensions (see the [build tool](building) for details) ns | the default namespace of the archive used for all files that do not declare a namespace ns-PREFIX | a namespace binding for PREFIX that is in effect for all files in the archives (unless a file redefines the prefix) -dependencies | comma-seperated dependencies for the archive in question. Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf). +dependencies | comma-separated dependencies for the archive in question. Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf). foundation | the (assumed to be common) **meta theory** for all modules in the archive. diff --git a/doc/development/contributing.md b/doc/development/contributing.md index 9882f7e..dab588f 100644 --- a/doc/development/contributing.md +++ b/doc/development/contributing.md @@ -73,7 +73,7 @@ There are two essential workflows: #### Updating the release branch -Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriatly. +Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriately. Once such a change has landed on master, when then again use pull requests to mark a version of MMT as a release. This time we merge from ```master``` onto ```release```. diff --git a/doc/development/releases.md b/doc/development/releases.md index 72d2241..04b278e 100644 --- a/doc/development/releases.md +++ b/doc/development/releases.md @@ -461,7 +461,7 @@ Released on [22nd February 2017](https://github.com/UniFormal/MMT/releases/tag/v * Initial version of Active Computation Extension * Improvements: * Update to Travis Build Scripts - * Webserver Improvements, including CORS support, hostname support, and client side libarary updates] + * Webserver Improvements, including CORS support, hostname support, and client side library updates] #### Release 4 diff --git a/doc/development/scala.md b/doc/development/scala.md index 9c9af0e..cf9297f 100644 --- a/doc/development/scala.md +++ b/doc/development/scala.md @@ -18,7 +18,7 @@ Configure your IDEs accordingly and do not change styling recklessly. All indentation must be by spaces (no tabs). The depth of indentation is not fixed. It is typically 2-4 spaces. -It does not have to be consistent throughtout a file. +It does not have to be consistent throughout a file. #### Imports diff --git a/doc/language/declarations.md b/doc/language/declarations.md index 310590f..472008c 100644 --- a/doc/language/declarations.md +++ b/doc/language/declarations.md @@ -120,7 +120,7 @@ The syntax for structures is * Even though structures are declarations, they have a [module](modules) body and are thus delimited by the module [delimiter](delimiters) ![`\GS`](../img/GS.png) instead of the declaration delimiter ![`\RS`](../img/RS.png). * Simple includes are still delimited with ![`\RS`](../img/RS.png). * The name of each declaration in a structure has to correspond to the name of a declaration in the ``. -* Components (aliases, types, definitions etc.) explicitely given in a structure *override* the corresponding component of the declaration in the ``, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration. +* Components (aliases, types, definitions etc.) explicitly given in a structure *override* the corresponding component of the declaration in the ``, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration. * The full [URI](uris) of an induced declaration `` in a structure `` in a module `` is ` ? / `. It is this declaration, that is visible from the outside and can be used in subsequent (to the structure) declarations. In contrast, the URI ` / ? ` refers to the plain declaration as declared *directly in the structure*, i.e. without inheritance. The latter should never be used outside of the [API](../api) and is invisible to declarations outside of the structure. * Unlike simple includes, multiple *named structures* with the same `` are **not** redundant. Each structure introduces fresh (possibly modified) copies of the declarations in the domain. * The limit of the previous point is the [*meta theory*](modules.html#theories) of the domain. If two structures `s1`,`s2` have corresponding domains `dom1`,`dom2` with the same meta theory `meta`, then *everything in the dependency closure of `meta`* will be included exactly once. diff --git a/doc/language/implicit.md b/doc/language/implicit.md index 737ca3f..5870185 100644 --- a/doc/language/implicit.md +++ b/doc/language/implicit.md @@ -23,7 +23,7 @@ If there is an implicit morphism m from S to T, all names c of S can be used in Similarly, every morphism out of T can be treated as a morphism out of S by composing with m. This happens automatically, i.e., the user does not have to refer to m, hence the name *implicit* morphisms. -Of course, this only works if m is uniuqe, i.e., there may at most 1 implicit morphism between any two theories. +Of course, this only works if m is unique, i.e., there may at most 1 implicit morphism between any two theories. In other words, the subgraph of implicit morphisms must commute. A number of examples are given in the research paper on implicit morphisms. @@ -177,7 +177,7 @@ MMT flattens every include i of S in T and by composing it with every include in The order is relevant because the declarations included by i can already be used in the declarations between i and a later include with the same domain. There is one relaxation though. -If the later include i2 of R is primitve, it can often be dropped even if an earlier include i1 of R has a different kind or a definition. +If the later include i2 of R is primitive, it can often be dropped even if an earlier include i1 of R has a different kind or a definition. This is justified because: * If i2 is a realization, the promise of i2 is trivial because it has already been fulfilled by i1. * If i2 is a plain include and i1 already provides a definition m, dropping i2 amounts to implicitly instantiating all R-constants in the domain of i2 via m. diff --git a/doc/language/index.md b/doc/language/index.md index 1fb63c0..b62a58e 100644 --- a/doc/language/index.md +++ b/doc/language/index.md @@ -5,7 +5,7 @@ title: The MMT Language This sections gives an overview of the **general language structure** of MMT. To be more concrete, it also explains one specific **concrete syntax**, which is the main syntax used to write MMT content natively. -A description of MMT's **abstract syntax** and the corrseponding internal data structures can be found [here](../api/syntax) +A description of MMT's **abstract syntax** and the corresponding internal data structures can be found [here](../api/syntax) MMT is a language for formal mathematics that pays special attention to [*foundation-independence*](../philosophy/independence), scalability, and modularity. MMT follows the [OMDoc](http://www.omdoc.org/) philosophy and will be integrated into the upcoming OMDoc 2 format. diff --git a/doc/language/inductive.md b/doc/language/inductive.md index 596df54..f6a81c0 100644 --- a/doc/language/inductive.md +++ b/doc/language/inductive.md @@ -5,7 +5,7 @@ title: Inductive Types ### Declaraing an inductive type -The structural feature **inductive** for inductive types can be used to elaborate to define (mutally) inductive types. A derived declaration for this features consists of: +The structural feature **inductive** for inductive types can be used to elaborate to define (mutually) inductive types. A derived declaration for this features consists of: * A name of the derived declaration * A list of parameters of the derived declaration (similar to theory parameters) @@ -13,7 +13,7 @@ The structural feature **inductive** for inductive types can be used to elaborat There are three types of internal declarations: -* Type-Level internal declarations declaring the (mutaully) inductively-defined types we want to define +* Type-Level internal declarations declaring the (mutually) inductively-defined types we want to define * The constructors of those types * Further outgoing termlevel declarations, i.e. for declaring additional properties of the inductive type @@ -34,8 +34,8 @@ Here we have a typelevel `` (of type ``), a constructor `` of `` * A declaration axiomatizing the definition for each constructor case diff --git a/doc/language/informal.md b/doc/language/informal.md index 96a6254..8c6361d 100644 --- a/doc/language/informal.md +++ b/doc/language/informal.md @@ -2,6 +2,6 @@ layout: doc title: Flexiformal Knowledge --- -Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematatical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. +Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. The bulk of flexiformalizations in the MMT world are generated from [sTeX](http://github.com/KWARC/sTeX), a semantics-enhanced version of LaTeX which can be [converted to](https://uniformal.github.io/doc/applications/stex) flexiformal MMT. Much of this content is hosted on [MathHub](http://mathhub.info). diff --git a/doc/language/modules.md b/doc/language/modules.md index 78e40d0..401242c 100644 --- a/doc/language/modules.md +++ b/doc/language/modules.md @@ -20,13 +20,13 @@ Theories can be *nested*, like this: ![`theory : = theory : = \GS \GS`](../img/nestedtheory.png) -in which case the visible context of both the inner theory as well as `` is ``, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitely [included](declarations.html#structures)). +in which case the visible context of both the inner theory as well as `` is ``, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitly [included](declarations.html#structures)). ### Views Given two theories `A` and `B`, a **view** from `A` to `B` maps all [declarations](declarations) in `A` to expressions over symbols in `B`, while preserving *typing judgments*. i.e. if `|- a : tpA` in `A` and `v:A->B` is a view, then `|- v(a) : v(tpA)`. Hence, views are *truth preserving*. `A` is the *domain* of `v` and `B` is the *codomain*. -Their conrete syntax is +Their concrete syntax is ![`view : -> = \GS`](../img/view.png) diff --git a/doc/philosophy/independence.md b/doc/philosophy/independence.md index e975fc7..1700667 100644 --- a/doc/philosophy/independence.md +++ b/doc/philosophy/independence.md @@ -12,6 +12,6 @@ MMT is an API and as such not committed to particular applications. The MMT system includes several [MMT-based applications](../applications/) that yield, e.g., [build tools](../archives/building) for [MMT archives](../archives), a [jEdit-based text editor](../applications/jedit), or a [web server](../applications/server) for MMT content. ### Logic Independence -MMT is logic-independent, i.e., it is not commited to a particular logic. +MMT is logic-independent, i.e., it is not committed to a particular logic. Therefore, MMT users have to define their logic in MMT or import a logic defined by someone else. MMT beginners should check out the [MMT archive](../archives) [urtheories](https://gl.mathhub.info/MMT/urtheories). This archive defines several basic languages, in particular the logical framework [**LF**](https://en.wikipedia.org/wiki/Logical_framework#LF). Other archives can be found at [OAF](../archives/oaf) diff --git a/doc/philosophy/papers.md b/doc/philosophy/papers.md index b168fda..a315bb8 100644 --- a/doc/philosophy/papers.md +++ b/doc/philosophy/papers.md @@ -18,7 +18,7 @@ Most relevant papers can be found in Florian Rabe's [publication list](https://k There is also an [entry](http://swmath.org/software/7136) for MMT in the swMath catalog of mathematical software. -* M. Kohlhase, F. Mance, F. Rabe, [A Universal Machine for Biform Theory Graphs](http://kwarc.info/frabe/Research/KMR_uom_13.pdf) - biform theories (deduction and computatiton) in MMT with a practical integration of MMT and Scala (published at CICM 2013) +* M. Kohlhase, F. Mance, F. Rabe, [A Universal Machine for Biform Theory Graphs](http://kwarc.info/frabe/Research/KMR_uom_13.pdf) - biform theories (deduction and computation) in MMT with a practical integration of MMT and Scala (published at CICM 2013) * D. Ginev, M. Iancu, F. Rabe, [Integrating Content and Narration-Oriented Document Formats](http://kwarc.info/frabe/Research/GIR_mmtlatex_13.pdf) - an integration between MMT and LaTeX * M. Iancu, M. Kohlhase, [Searching the Space of Mathematical Knowledge](http://www.cicm-conference.org/2012/mir/mir2012_submission_5.pdf) - this application uses MMT to generate smart search indices that include inherited and computed knowledge (published at MIR 2012) * M. Iancu, F. Rabe, [Work-in-progress: An MMT-Based User-Interface](http://kwarc.info/frabe/Research/IR_ui_12.pdf) - a summary of the state of editing in MMT (published at UITP 2012) diff --git a/doc/setup/configure.md b/doc/setup/configure.md index c22c430..02d81ee 100644 --- a/doc/setup/configure.md +++ b/doc/setup/configure.md @@ -11,7 +11,7 @@ When started, MMT looks for a configuration file called `mmtrc` in the following Later configuration entries overwrite earlier ones. -During setup a defaut configuration file is generated and placed in the `deploy` folder. +During setup a default configuration file is generated and placed in the `deploy` folder. That file also includes some example configuration entries. ### Configuration File Syntax diff --git a/doc/setup/devel.md b/doc/setup/devel.md index 5629185..3ef3409 100644 --- a/doc/setup/devel.md +++ b/doc/setup/devel.md @@ -3,7 +3,7 @@ layout: doc title: Developing MMT --- -For developing and building MMT, it is recommened to use IntelliJ IDEA or Eclipse. +For developing and building MMT, it is recommended to use IntelliJ IDEA or Eclipse. Furthermore, a working installation of `sbt` is required. ### Using IntelliJ IDEA diff --git a/doc/setup/docker.md b/doc/setup/docker.md index 673e2b4..447714d 100644 --- a/doc/setup/docker.md +++ b/doc/setup/docker.md @@ -15,7 +15,7 @@ To start a temporary container with permanent volume for MMT content, use: ``` This will run the newest MMT.jar and store all archives inside a new volume called mmt mounted under `/content/`. -The command can be run multiple times to (re-)start the container if neccessary. +The command can be run multiple times to (re-)start the container if necessary. ### Storage diff --git a/doc/setup/repo.md b/doc/setup/repo.md index 59e3659..d51b04a 100644 --- a/doc/setup/repo.md +++ b/doc/setup/repo.md @@ -11,7 +11,7 @@ The content of the subdirectories is as follows: Their status is somewhat between release and nightly build: I commit new builts frequently, and they are usually stable. The subfolders are * `main`: all jar files of MMT projects - * `lib`: all jar files that MMT depends on, including the Scala library The only extenal dependency is the JVM itself. For most parts, Java 6 is fine; occassionally Java 7 is needed. The run scripts automatically put all necessary jars on the Java classpath. + * `lib`: all jar files that MMT depends on, including the Scala library The only extenal dependency is the JVM itself. For most parts, Java 6 is fine; occasionally Java 7 is needed. The run scripts automatically put all necessary jars on the Java classpath. * `lfcatalog`: the jar files of the LF catalog, to be used with Twelf * `jedit-plugin`: all jar and other files needed for the plugin for jEdit * `src/`: All sources. diff --git a/doc/setup/running.md b/doc/setup/running.md index 13a93cb..c1fb22a 100644 --- a/doc/setup/running.md +++ b/doc/setup/running.md @@ -62,7 +62,7 @@ The `deploy` folder contains shell scripts that automate running from these smal * `mmt` (for Unix) and `mmt.bat` (for Windows): executes MMT commands and/or opens an [MMT shell](../applications/shell), `mmt -help` displays the available options * `run-file.bat`: a convenience script for Windows that can be associated with MMT shell scripts. -Users may wish to add the deploy folder to the PATH enviroment variable. +Users may wish to add the deploy folder to the PATH environment variable. #### Running from Classes diff --git a/doc/tutorials/jedit/3LF.md b/doc/tutorials/jedit/3LF.md index a434550..fffa987 100644 --- a/doc/tutorials/jedit/3LF.md +++ b/doc/tutorials/jedit/3LF.md @@ -64,7 +64,7 @@ The last point is worth looking at more closely: Usually, proof rules are denote In the case of propositional logic, we have a single judgment for every proposition `φ:prop`, namely the judgment `⊦ φ` that `φ` holds. Correspondingly, we declared the function `proof`, that maps a proposition `φ` to the associated type of proofs `⊦ φ`. The syntax we have already taken care of, by declaring the connectives as functions on the type `prop`. -In the next section we will use dependend function types to implement the rules of the *natural deduction* calculus as functions, that yield elements of the proof types `⊦ φ`. +In the next section we will use dependent function types to implement the rules of the *natural deduction* calculus as functions, that yield elements of the proof types `⊦ φ`. ------------------------------- diff --git a/doc/tutorials/jedit/4natded.md b/doc/tutorials/jedit/4natded.md index f26e15a..5f872e3 100644 --- a/doc/tutorials/jedit/4natded.md +++ b/doc/tutorials/jedit/4natded.md @@ -29,19 +29,19 @@ Since we use judgments-as-types, these three rules correspond to the following t ![`\vdash A \wedge B \to \vdash A`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20A) ![`\vdash A \wedge B \to \vdash B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20B) -Noticably, the function arrows in these types lend themselves to be interpreted just like implications: We can read e.g. the first rule as +Noticeably, the function arrows in these types lend themselves to be interpreted just like implications: We can read e.g. the first rule as > If `A` is provable, then (if `B` is provable, then `A∧B` is provable). This is no coincidence - this correspondence between a logical connective and a type constructor is known as *Curry-Howard-Isomorphism* (or *propositions-as-types*), and we will (rather trivially) prove this isomorphism later in MMT using [views](../../language/modules.html#views). -However, the types above don't quite work in LF, for the simple reason, that `A` and `B` are free variables. The proof rules are valid for *any* propositions `A`, `B`, so to avoid them being free variables, we can instead declare a *function* that takes two proposition `A`,`B` and returns the functions corresponding to the rules. For that, we finally need the dependend function types: +However, the types above don't quite work in LF, for the simple reason, that `A` and `B` are free variables. The proof rules are valid for *any* propositions `A`, `B`, so to avoid them being free variables, we can instead declare a *function* that takes two proposition `A`,`B` and returns the functions corresponding to the rules. For that, we finally need the dependent function types: ![`\prod_{A:prop}\prod_{B:prop}\vdash A \to \vdash B \to \vdash A\wedge B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5C%3B%20%5Cto%5C%3B%20%5Cvdash%20B%5C%3B%5Cto%5C%3B%5Cvdash%20A%5Cwedge%20B) ![`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash A`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20A) ![`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20B) -Again, noticably, the dependent functions here lend themselves to be read like a "for all" - e.g. we can read the first rule as +Again, noticeably, the dependent functions here lend themselves to be read like a "for all" - e.g. we can read the first rule as > For all `A:prop`, for all `B:prop`: If `A` is provable, then (if `B` is provable, then `A∧B` is provable). diff --git a/doc/tutorials/prototyping/index.md b/doc/tutorials/prototyping/index.md index 5dff0d8..e44093d 100644 --- a/doc/tutorials/prototyping/index.md +++ b/doc/tutorials/prototyping/index.md @@ -9,7 +9,7 @@ The complete files built interactively in this tutorial can be found at https:// It assumes that * MMT has been [installed](../../setup), -* archives are placed in some folder, which is refered to as `CONTENT`,The MMT installer should take care of this +* archives are placed in some folder, which is referred to as `CONTENT`,The MMT installer should take care of this * [jEdit](../../applications/jedit) is used for editing mmt files.Other editors will work but might make editing awkward. ### Define a Meta-Logic diff --git a/doc/tutorials/slides/applications.tex b/doc/tutorials/slides/applications.tex index 4208f31..6e4d330 100644 --- a/doc/tutorials/slides/applications.tex +++ b/doc/tutorials/slides/applications.tex @@ -119,7 +119,7 @@ \section{Breadth of Possible Applications} Design: MMT as p MMT and jEdit \begin{itemize} - \item Plugin for jEdit that wraps arond MMT + \item Plugin for jEdit that wraps around MMT \item MMT and jEdit large projects \item But only little glue code needed \lec{mostly forwarding to MMT API functions}