More tests for structural features.

parent 90aeafe4
namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
theory LFEq =
include ur:?LF
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://induction.lf.mmt.kwarc.info❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
theory LFI =
include ur:?LF
rule rules?InductiveRule
include ur:?LF
rule rules?InductiveTypes ❙

theory NatExample : ?LFI =
inductive nat =
n: type
z: n
s: n ⟶ n

rule rules?InductiveTypes ❙

theory TestExample : ?LFI =
rule rules?InductiveTypes ❙
m : type ❙
bla : type ❙
inductive stressTest(R: type) ❘ =
a: type ❙
r : type ❙
b: {x:a} type ❙
c: {x:a, y: b x} type ❘ # 1 ° 2 ❙
// This currently works, but is problematic when inductive types are elaborated to defined derived declarations ❙
d: bla ⟶ r ⟶ bla ❙
e: r ⟶ bla ⟶ r ❘ # 1 e 2 ❙
f: bla ⟶ r ❙
k: bla ❙
l: {x:a} b x ❙
m: {x:a, y: b x} c x y ❙
n: {x:a} a ❙
o: {x:a, y: b x} c x y ⟶ a ❙
p: {x:a, y: b x} b x ⟶ c x y ❙
q: {x:a} a ⟶ b x ❙


namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
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