Skip to content
Snippets Groups Projects
Commit 60fb75d5 authored by Dennis Müller's avatar Dennis Müller
Browse files

generated files

parent 029d72e2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz
+ 0
− 0
View file @ 60fb75d5
No preview for this file type
narration/math.omdoc
+ 1
− 1
View file @ 60fb75d5
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/Foundation/math.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#0.0.0:11364.342.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/Foundation"/><instruction text="import rules scala://rules.mitm.mmt.kwarc.info"/><instruction text="import lf scala://lf.mmt.kwarc.info/"/><instruction text="import lfx scala://LFX.mmt.kwarc.info"/><instruction text="fixmeta http://cds.omdoc.org/mmt?mmt"/><mref name="[http://mathhub.info/MitM/Foundation?Metadata]" target="http://mathhub.info/MitM/Foundation?Metadata"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#217.8.0:231.8.14"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#261.12.0:330.12.69"/></metadata>We define a formal language for basic mathematical objects in LF.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Subtyping]" target="http://mathhub.info/MitM/Foundation?Subtyping"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#333.14.0:348.14.15"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#420.18.0:442.18.22"/></metadata>First, some logic.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Logic]" target="http://mathhub.info/MitM/Foundation?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#493.21.0:504.21.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?NaturalDeduction]" target="http://mathhub.info/MitM/Foundation?NaturalDeduction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#2741.70.0:2763.70.22"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#4563.108.0:4744.109.106"/></metadata>Now some theories that introduce primitive types and literals for them.
<omdoc base="http://mathhub.info/MitM/Foundation/math.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#0.0.0:11364.342.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/Foundation"/><instruction text="import rules scala://rules.mitm.mmt.kwarc.info"/><instruction text="import lf scala://lf.mmt.kwarc.info"/><instruction text="import lfx scala://LFX.mmt.kwarc.info"/><instruction text="fixmeta http://cds.omdoc.org/mmt?mmt"/><mref name="[http://mathhub.info/MitM/Foundation?Metadata]" target="http://mathhub.info/MitM/Foundation?Metadata"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#217.8.0:231.8.14"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#261.12.0:330.12.69"/></metadata>We define a formal language for basic mathematical objects in LF.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Subtyping]" target="http://mathhub.info/MitM/Foundation?Subtyping"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#333.14.0:348.14.15"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#420.18.0:442.18.22"/></metadata>First, some logic.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Logic]" target="http://mathhub.info/MitM/Foundation?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#493.21.0:504.21.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?NaturalDeduction]" target="http://mathhub.info/MitM/Foundation?NaturalDeduction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#2741.70.0:2763.70.22"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#4563.108.0:4744.109.106"/></metadata>Now some theories that introduce primitive types and literals for them.
Because literals must modify the parser, they are supplied as rules that are implemented in a plugin.</opaque><mref name="[http://mathhub.info/MitM/Foundation?NatLiterals]" target="http://mathhub.info/MitM/Foundation?NatLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#4753.111.0:4770.111.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?IntLiterals]" target="http://mathhub.info/MitM/Foundation?IntLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#5609.139.0:5626.139.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?RealLiterals]" target="http://mathhub.info/MitM/Foundation?RealLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#5982.155.0:6000.155.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Literals]" target="http://mathhub.info/MitM/Foundation?Literals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#6558.176.0:6572.176.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Trigonometry]" target="http://mathhub.info/MitM/Foundation?Trigonometry"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7045.197.0:7063.197.18"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7466.217.0:7534.217.68"/></metadata>String literals are also needed occasionally, e.g., in the LMFDB.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Strings]" target="http://mathhub.info/MitM/Foundation?Strings"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7538.219.0:7551.219.13"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7670.226.0:7714.226.44"/></metadata>Now some more complex types. First lists.</opaque><mref name="[http://mathhub.info/MitM/Foundation?Lists]" target="http://mathhub.info/MitM/Foundation?Lists"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7717.228.0:7728.228.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?InformalProofs]" target="http://mathhub.info/MitM/Foundation?InformalProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#7807.232.0:7827.232.20"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#8093.242.0:8331.250.0"/></metadata><scope>(Finite) sets ❙
theory Sets : ur:?LF =
include ?Logic❙
......
relational/http..mathhub.info/MitM/Foundation/$Logic.rel
+ 2
− 2
View file @ 60fb75d5
......@@ -35,8 +35,8 @@ DependsOn http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type http://cd
DependsOn http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
Declares http://mathhub.info/MitM/Foundation?Logic http://mathhub.info/MitM/Foundation?Logic?[scala://lf.mmt.kwarc.info/?TermIrrelevanceRule]/-975443801
constant http://mathhub.info/MitM/Foundation?Logic?[scala://lf.mmt.kwarc.info/?TermIrrelevanceRule]/-975443801
Declares http://mathhub.info/MitM/Foundation?Logic http://mathhub.info/MitM/Foundation?Logic?[scala://lf.mmt.kwarc.info?TermIrrelevanceRule]/-975443801
constant http://mathhub.info/MitM/Foundation?Logic?[scala://lf.mmt.kwarc.info?TermIrrelevanceRule]/-975443801
Declares http://mathhub.info/MitM/Foundation?Logic http://mathhub.info/MitM/Foundation?Logic?eq
constant http://mathhub.info/MitM/Foundation?Logic?eq
DependsOn http://mathhub.info/MitM/Foundation?Logic?eq?type http://mathhub.info/MitM/Foundation?Logic?prop?type
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment