blob: 83fb3d0c8ed27c9139f17d45bed224739cce8a6c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
From Coq Require Program.
Section Scope.
#[local] Coercion nat_of_bool (b: bool) : nat :=
if b then 0 else 1.
Check (refl_equal : true = 0 :> nat).
End Scope.
Fail Check 0 = true :> nat.
#[polymorphic]
Definition ι T (x: T) := x.
Check ι _ ι.
#[program]
Fixpoint f (n: nat) {wf lt n} : nat := _.
#[deprecated(since="8.9.0")]
Ltac foo := foo.
|
