32 lines
535 B
Plaintext
32 lines
535 B
Plaintext
// Simpler sort parameter test
|
|
|
|
theory (X : Sort) Container {
|
|
elem : X; // not a Sort, but an element of X
|
|
}
|
|
|
|
// Hmm, this doesn't quite work...
|
|
// Let me try the actual vision pattern
|
|
|
|
theory Base {
|
|
A : Sort;
|
|
B : Sort;
|
|
}
|
|
|
|
instance MyBase : Base = {
|
|
a1 : A;
|
|
a2 : A;
|
|
b1 : B;
|
|
b2 : B;
|
|
}
|
|
|
|
// Now try a theory parameterized by an instance
|
|
theory (Inst : Base instance) Map {
|
|
map : Inst/A -> Inst/B;
|
|
}
|
|
|
|
// Instance of Map parameterized by MyBase
|
|
instance MyMap : MyBase Map = {
|
|
a1 map = MyBase/b1;
|
|
a2 map = MyBase/b2;
|
|
}
|