blob: b8db52735da5de1cbefd92346f0adedac9683f32 (
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
29
30
|
Axioms:
foo : nat
Axioms:
foo : nat
Axioms:
bli : Type
Axioms:
bli : Type
Axioms:
seq relies on definitional UIP.
Axioms:
extensionality
: forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
Axioms:
extensionality
: forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
Axioms:
extensionality
: forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
Axioms:
extensionality
: forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
Closed under the global context
Closed under the global context
Axioms:
M.foo : False
Closed under the global context
Closed under the global context
Closed under the global context
Closed under the global context
|
