blob: b1d2a54f25c7c3cd144264ab5317b2b58e537fcb (
plain)
1
2
3
4
5
|
Record a_struct := { anum : nat }.
Canonical Structure a_struct_0 := {| anum := 0|}.
Definition rename_a_s_0 := a_struct_0.
Coercion some_nat := (@Some nat).
Definition rename_some_nat := some_nat.
|