blob: 4c221dc7f10536ef0e6b2af0f0fb675cca5d75ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
Axiom SProp : Set.
Axiom sp : SProp.
(* If we hardcode valueType := nat, it goes through *)
Class StateIs := {
valueType : Type;
stateIs : valueType -> SProp
}.
Instance NatStateIs : StateIs := {
valueType := nat;
stateIs := fun _ => sp
}.
Class LogicOps F := { land: F -> F }.
Instance : LogicOps SProp. Admitted.
Instance : LogicOps Prop. Admitted.
Set Printing All.
Parameter (n : nat).
(* If this is a [Definition], the resolution goes through fine. *)
Notation vn := (@stateIs _ n).
Definition vn' := (@stateIs _ n).
Definition GOOD : SProp :=
@land _ _ vn'.
(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
Fail Definition BAD : SProp :=
@land _ _ vn.
|
