Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Search is:Scheme lists inductives not schemes #18298

Closed
SkySkimmer opened this issue Nov 10, 2023 · 0 comments · Fixed by #18299 or #18537
Closed

Search is:Scheme lists inductives not schemes #18298

SkySkimmer opened this issue Nov 10, 2023 · 0 comments · Fixed by #18299 or #18537
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc.
Milestone

Comments

@SkySkimmer
Copy link
Contributor

Search is:Scheme.
(* 
Number.number: Set
Number.signed_int: Set
Number.uint: Set
False: Prop
True: Prop
Hexadecimal.hexadecimal: Set
Decimal.decimal: Set
Decimal.signed_int: Set
Hexadecimal.signed_int: Set
Hexadecimal.uint: Set
nat: Set
bool: Set
Decimal.uint: Set
comparison: Set
unit: Set
Empty_set: Set
Byte.byte: Set
list: Type -> Type
option: Type -> Type
inhabited: Type -> Prop
or: Prop -> Prop -> Prop
and: Prop -> Prop -> Prop
sumor: Type -> Prop -> Type
sumbool: Prop -> Prop -> Set
prod: Type -> Type -> Type
sum: Type -> Type -> Type
eq_true: bool -> Prop
sig: forall [A : Type], (A -> Prop) -> Type
sigT: forall [A : Type], (A -> Type) -> Type
ex: forall [A : Type], (A -> Prop) -> Prop
eq: forall {A : Type}, A -> A -> Prop
le: nat -> nat -> Prop
BoolSpec: Prop -> Prop -> bool -> Prop
sigT2: forall [A : Type], (A -> Type) -> (A -> Type) -> Type
ex2: forall [A : Type], (A -> Prop) -> (A -> Prop) -> Prop
Acc: forall [A : Type], (A -> A -> Prop) -> A -> Prop
sig2: forall [A : Type], (A -> Prop) -> (A -> Prop) -> Type
CompareSpecT: Prop -> Prop -> Prop -> comparison -> Set
CompareSpec: Prop -> Prop -> Prop -> comparison -> Prop
*)
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Nov 10, 2023
@SkySkimmer SkySkimmer added kind: user messages Improvement of error messages, new warnings, etc. kind: bug An error, flaw, fault or unintended behaviour. labels Nov 14, 2023
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Nov 21, 2023
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 23, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 23, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 23, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 24, 2024
@coqbot-app coqbot-app bot added this to the 8.20+rc1 milestone Feb 7, 2024
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant