CODEWITHSUNDEEP
coq
Siddharth Bhat
Siddharth Bhat

Reputation: 843

Scopes in Coq - importing without resolution?

Consider the sample code:

Require Import BinNat.
Open Scope N.

Check (N.ones).
(* Error: The reference ones
   was not found in the current environment. *)
Check (ones).

How do I import BinNat in such a way that I don't have to resolve ones to N.ones?

Upvotes: 0

Views: 112

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

The Import command can help:

From Coq Require Import BinNat.
Import N.
About ones.

Upvotes: 1

Related Questions