All Questions
Tagged with notation rocq-prover
22 questions
0
votes
1
answer
52
views
Why doesn't Coq notation defined by other notation working well?
Here is my Coq code.
I expected Check x ∪ y. shows x ∪ y but ∪ {x, y}.
Why? Or is there another idea to define notation?
My Coq version is 8.16.1.
Section Test.
Variable set:Type.
Variable In : ...
2
votes
1
answer
240
views
Is it possible to declare type-dependent Notation in Coq?
As Coq has a powerful type inference algorithm, I am wondering whether we can "overload" notations for different rewriting based on the Notation's variables.
As an example, I will borrow a ...
2
votes
1
answer
65
views
Why does an "only printing" notation modify the parser
The manual says that
If a given notation string occurs only in only printing rules, the parser is not modified at all.
So I would expect that when I add an "only printing" notation, the ...
1
vote
1
answer
153
views
Error when defining custom notation for an embedded logic
I'm working on a colleague's embedding of modal logic in Coq and I'm trying to define a custom notation for formulas of said logic, like presented here and also on Volume 2 of the book Software ...
- 41
1
vote
1
answer
51
views
Issue on definition expansion from Coq module system
I have defined a couple of modules in Coq to build a Byte type from a Bit type, recursively, as a three of pairs. But I hit an issue defining a Numeral Notation for the Byte type.
Here is the code:
...
- 1,904
3
votes
1
answer
566
views
Coq: About "%" and "mod" as a notation symbol
I'm trying to define a notation for modulo equivalence relation:
Inductive mod_equiv : nat -> nat -> nat -> Prop :=
| mod_intro_same : forall m n, mod_equiv m n n
| mod_intro_plus_l : ...
- 982
4
votes
1
answer
884
views
Do not import notations in coq
I have two external modules(the sources of which are better not to be alternated) which define the same notation. The consequence of this is I am now not able to import both module at the same time ...
- 6,333
4
votes
2
answers
411
views
Using Implicit Type Class Parameters in Coq Notation
I'm trying to wrap my head around type classes in Coq (I've dabbled with it in the past, but I'm a far cry from being an experienced user). As an exercise, I am trying to write a group theory library. ...
- 362
2
votes
1
answer
1k
views
Using a 3 symbols notation [constr:operconstr] expected after [constr:operconstr]
Say I have a relation and its reflexive and transitive closure (with n counting the number of "transitive steps":
Variable A: Type.
Inductive Relation: A -> A -> Prop :=
| rel: forall (a b: A)...
- 1,138
0
votes
1
answer
303
views
Coq: Fixing a recursive notation
Below is a half-working simple recursive notation:
Universe ARG. Definition ARG := Type@{ARG}.
Parameter X: ARG.
Notation A := (fun x:ARG->ARG => fun y:x X => y).
Parameter P: ARG -> ARG.
...
- 990
0
votes
0
answers
94
views
Coq: Defining multiple notations simultaneously
Is it possible to (somehow) define multiple notations simultaneously, e.g.
Notation (A|B) := nat.
or
Notation B := A
where A := nat.
The following works (but is not what I'm looking for; I want a "...
- 990
2
votes
1
answer
242
views
Coq: Defining a prefix notation
I've tried w/ different symbols but cannot get my prefix notation to work (infix, on the other hand, works). I guess it's a level problem but couldn't sort it out. Any ideas?
Variable (X R: Type)(x:X)...
- 990
2
votes
1
answer
409
views
Multiple Where-clauses for Reserved Notation in Coq?
I've got a bunch of mutually-inductive datatypes declared using with, and I'd like to define a Notation for each of them that I can use while I'm defining them.
I'm aware of Reserved Notations and ...
- 8,453
4
votes
1
answer
949
views
Syntax Error with `<` in Coq Notations
The following code:
Reserved Notation "g || t |- x < y" (at level 10).
Inductive SubtypeOf :
GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
forall (gamma ...
- 8,453
3
votes
1
answer
196
views
Can I use a notation for an Inductive type to define that type in Coq?
Suppose I've got something like this:
Inductive SubtypeOf :
Gamma -> UnsafeType -> Type -> Set :=
| SubRefl :
forall (gamma : GammaEnv) (u : UnsafeType)
, SubtypeOf gamma u u
| ...
- 8,453