Skip to content
Snippets Groups Projects
Commit 39d83f06 authored by ComFreek's avatar ComFreek
Browse files

switch to urtheories strings

parent d0cfa926
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 12 additions and 22 deletions
content/http..mathhub.info/MitM/Foundation/$Description$Operator.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Inductive$Types.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Informal$Proofs.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Lists.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Math.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Matrices.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Option$Type.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Sequences.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Strings.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
content/http..mathhub.info/MitM/Foundation/$Vectors.omdoc.xz
+ 0
− 0
View file @ 39d83f06
No preview for this file type
narration/math.omdoc
+ 4
− 4
View file @ 39d83f06
<?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:13021.380.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#419.18.0:441.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#492.21.0:503.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#2696.70.0:2718.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#6225.146.0:6406.147.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#6415.149.0:6432.149.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#7271.177.0:7288.177.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#7644.193.0:7662.193.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#8220.214.0:8234.214.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#8706.235.0:8724.235.18"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9126.255.0:9194.255.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#9198.257.0:9211.257.13"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9328.264.0:9372.264.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#9375.266.0:9386.266.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#9465.270.0:9485.270.20"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9750.280.0:9988.288.0"/></metadata><scope>(Finite) sets ❙
<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:12957.378.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#419.18.0:441.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#492.21.0:503.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#2696.70.0:2718.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#6225.146.0:6406.147.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#6415.149.0:6432.149.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#7271.177.0:7288.177.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#7644.193.0:7662.193.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#8220.214.0:8234.214.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#8706.235.0:8724.235.18"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9126.255.0:9194.255.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#9198.257.0:9211.257.13"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9251.261.0:9295.261.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#9298.263.0:9309.263.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#9388.267.0:9408.267.20"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9686.278.0:9924.286.0"/></metadata><scope>(Finite) sets ❙
theory Sets : ur:?LF =
include ?Logic❙
/T the type operator of sets along with its constructors❙
set: type ⟶ type ❙
empty: <scope>A</scope> (list A) ❘# ∅ 1❘## ∅ %I1 ❙
cons: <scope>A</scope> A ⟶ (list A) ⟶ (list A)❘ # 2 , 3 ❙</scope></opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9991.290.0:10125.294.41"/></metadata><scope>Multisets ❙
cons: <scope>A</scope> A ⟶ (list A) ⟶ (list A)❘ # 2 , 3 ❙</scope></opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#9927.288.0:10061.292.41"/></metadata><scope>Multisets ❙
/T Finite hybrid sets (mutlisets with possibly negative mutliplicities) ❙
/T Now vectors, i.e., fixed-length lists.</scope></opaque><mref name="[http://mathhub.info/MitM/Foundation?Vectors]" target="http://mathhub.info/MitM/Foundation?Vectors"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10128.296.0:10141.296.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Matrices]" target="http://mathhub.info/MitM/Foundation?Matrices"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10475.307.0:10489.307.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?OptionType]" target="http://mathhub.info/MitM/Foundation?OptionType"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10680.315.0:10696.315.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?DescriptionOperator]" target="http://mathhub.info/MitM/Foundation?DescriptionOperator"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#11219.331.0:11244.331.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?ProductTypes]" target="http://mathhub.info/MitM/Foundation?ProductTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12011.346.0:12029.346.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?FiniteTypes]" target="http://mathhub.info/MitM/Foundation?FiniteTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12141.349.0:12158.349.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?InductiveTypes]" target="http://mathhub.info/MitM/Foundation?InductiveTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12213.350.0:12233.350.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Sequences]" target="http://mathhub.info/MitM/Foundation?Sequences"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12311.354.0:12326.354.15"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12582.363.0:12671.363.89"/></metadata>Finally, a theory that puts everything together (not recommended, because modularity)</opaque><mref name="[http://mathhub.info/MitM/Foundation?Math]" target="http://mathhub.info/MitM/Foundation?Math"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12674.365.0:12684.365.10"/></metadata></mref></omdoc>
\ No newline at end of file
/T Now vectors, i.e., fixed-length lists.</scope></opaque><mref name="[http://mathhub.info/MitM/Foundation?Vectors]" target="http://mathhub.info/MitM/Foundation?Vectors"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10064.294.0:10077.294.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Matrices]" target="http://mathhub.info/MitM/Foundation?Matrices"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10411.305.0:10425.305.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?OptionType]" target="http://mathhub.info/MitM/Foundation?OptionType"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#10616.313.0:10632.313.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?DescriptionOperator]" target="http://mathhub.info/MitM/Foundation?DescriptionOperator"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#11155.329.0:11180.329.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?ProductTypes]" target="http://mathhub.info/MitM/Foundation?ProductTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#11947.344.0:11965.344.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?FiniteTypes]" target="http://mathhub.info/MitM/Foundation?FiniteTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12077.347.0:12094.347.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?InductiveTypes]" target="http://mathhub.info/MitM/Foundation?InductiveTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12149.348.0:12169.348.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/Foundation?Sequences]" target="http://mathhub.info/MitM/Foundation?Sequences"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12247.352.0:12262.352.15"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12518.361.0:12607.361.89"/></metadata>Finally, a theory that puts everything together (not recommended, because modularity)</opaque><mref name="[http://mathhub.info/MitM/Foundation?Math]" target="http://mathhub.info/MitM/Foundation?Math"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Foundation/math.mmt#12610.363.0:12620.363.10"/></metadata></mref></omdoc>
\ No newline at end of file
relational/http..mathhub.info/MitM/Foundation/$Informal$Proofs.rel
+ 3
− 2
View file @ 39d83f06
......@@ -4,6 +4,7 @@ dataconstructor http://mathhub.info/MitM/Foundation?InformalProofs?addproofstep
dataconstructor http://mathhub.info/MitM/Foundation?InformalProofs?trivial
theory http://mathhub.info/MitM/Foundation?InformalProofs
HasMeta http://mathhub.info/MitM/Foundation?InformalProofs http://cds.omdoc.org/urtheories?LF
Includes http://mathhub.info/MitM/Foundation?InformalProofs http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/Foundation?InformalProofs http://mathhub.info/MitM/Foundation?Strings
Declares http://mathhub.info/MitM/Foundation?InformalProofs http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch
constant http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch
......@@ -11,7 +12,7 @@ DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type ht
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type http://mathhub.info/MitM/Foundation?Strings?string?type
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type http://cds.omdoc.org/urtheories?Strings?string?type
Declares http://mathhub.info/MitM/Foundation?InformalProofs http://mathhub.info/MitM/Foundation?InformalProofs?byproof
constant http://mathhub.info/MitM/Foundation?InformalProofs?byproof
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?byproof?type http://cds.omdoc.org/urtheories?Bool?BOOL?type
......@@ -37,4 +38,4 @@ DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition http://cds.omdoc.org/urtheories?Ded?DED?type
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition http://mathhub.info/MitM/Foundation?Strings?string?type
DependsOn http://mathhub.info/MitM/Foundation?InformalProofs?trivial?definition http://cds.omdoc.org/urtheories?Strings?string?type
relational/http..mathhub.info/MitM/Foundation/$Strings.rel
+ 1
− 10
View file @ 39d83f06
datatypeconstructor http://mathhub.info/MitM/Foundation?Strings?string
dataconstructor http://mathhub.info/MitM/Foundation?Strings?concat
theory http://mathhub.info/MitM/Foundation?Strings
HasMeta http://mathhub.info/MitM/Foundation?Strings http://cds.omdoc.org/urtheories?LF
Includes http://mathhub.info/MitM/Foundation?Strings http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/Foundation?Strings http://mathhub.info/MitM/Foundation?Strings?string
constant http://mathhub.info/MitM/Foundation?Strings?string
Declares http://mathhub.info/MitM/Foundation?Strings http://mathhub.info/MitM/Foundation?Strings?[scala://rules.mitm.mmt.kwarc.info?StringLiterals]
constant http://mathhub.info/MitM/Foundation?Strings?[scala://rules.mitm.mmt.kwarc.info?StringLiterals]
Declares http://mathhub.info/MitM/Foundation?Strings http://mathhub.info/MitM/Foundation?Strings?concat
constant http://mathhub.info/MitM/Foundation?Strings?concat
DependsOn http://mathhub.info/MitM/Foundation?Strings?concat?type http://mathhub.info/MitM/Foundation?Strings?string?type
Includes http://mathhub.info/MitM/Foundation?Strings http://cds.omdoc.org/urtheories?Strings
source/math.mmt
+ 4
− 6
View file @ 39d83f06
......@@ -256,10 +256,7 @@ theory Trigonometry : ur:?LF =
/T String literals are also needed occasionally, e.g., in the LMFDB.❚
theory Strings : ur:?LF =
include ?Logic❙
string: type ❙
rule rules?StringLiterals ❙
concat: string ⟶ string ⟶ string❙
include ☞ur:?Strings ❙
❚
/T Now some more complex types. First lists.❚
......@@ -269,8 +266,9 @@ theory Lists : ur:?LF =
❚
theory InformalProofs : ur:?LF =
include ?Strings ❙
include ?Logic ❙
include ?Strings ❙
proofsketch : {A : prop} string ⟶ ⊦ A ❘ # sketch 2 ❙
byproof : {A,B} ⊦ A ⟶ ⊦ B ❘ # by 3 ❙
addproofstep : {A,B,C: prop} ⊦ A ⟶ ⊦ B ⟶ ⊦ B ❘ # 4 and 5 ❙
......
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