blob: 5f575d5fe0f839c3404bd2d3aa5aea197a0537fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
let signature S = (n : Nat) -> Set
let signature U = (k : Bool) -> S
let signature W = (k : Bool)(n : Nat) -> Set
let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set)
let instance w :: W = u
let signature F = (n : Nat) (m : Nat) -> Set
let signature G = (n : Nat) -> (m : Nat) -> Set
let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set)
let instance g :: G = f
|
