Commit 28b9710e authored by Florian Rabe's avatar Florian Rabe

no message

parent b263c07b
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/linear.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#0.0.0:5169.158.0"/></metadata><mref name="[http://cds.omdoc.org/examples/linear?Syntax]" target="http://cds.omdoc.org/examples/linear?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#327.10.0:339.10.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Worlds]" target="http://cds.omdoc.org/examples/linear?Worlds"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#664.25.0:676.25.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Exchange]" target="http://cds.omdoc.org/examples/linear?Exchange"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1331.46.0:1345.46.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Contraction]" target="http://cds.omdoc.org/examples/linear?Contraction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1581.57.0:1598.57.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Weakening]" target="http://cds.omdoc.org/examples/linear?Weakening"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1708.63.0:1723.63.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?ResourceSemantics]" target="http://cds.omdoc.org/examples/linear?ResourceSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#2101.74.0:2124.74.23"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/logic/linear.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#0.0.0:5195.158.0"/></metadata><mref name="[http://cds.omdoc.org/examples/linear?Syntax]" target="http://cds.omdoc.org/examples/linear?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#327.10.0:339.10.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Worlds]" target="http://cds.omdoc.org/examples/linear?Worlds"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#664.25.0:676.25.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Exchange]" target="http://cds.omdoc.org/examples/linear?Exchange"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1331.46.0:1345.46.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Contraction]" target="http://cds.omdoc.org/examples/linear?Contraction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1581.57.0:1598.57.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Weakening]" target="http://cds.omdoc.org/examples/linear?Weakening"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1708.63.0:1723.63.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?ResourceSemantics]" target="http://cds.omdoc.org/examples/linear?ResourceSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#2124.74.0:2147.74.23"/></metadata></mref></omdoc>
\ No newline at end of file
namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
// temporary experiment by Colin ❚
theory LFEq =
include ur:?PLF
rule rules?EquivalenceRelation 

theory trivialEquivExample : ?LFEq =
rule rules?EquivalenceRelation 
true : type 
trivial_relation: {A: type} A ⟶ A ⟶ type ❘ = [A: type, a:A, b:A] true 
equivRel trivExam(A:type) ❘ =
triv_rel: A ⟶ A ⟶ type ❘// = [a:A, b:A] true 

namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
// temporary experiment by Colin ❚
theory LFEq =
include ur:?LF
rule rules?EquivalenceRelation 
rule rules?Quotients 

theory trivialQuotExample : ?LFEq =
rule rules?EquivalenceRelation 
rule rules?Quotients 
true : type 
quotient trivialExam(A: type) ❘ =
triv_rel: A ⟶ A ⟶ type ❙


Markdown is supported
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