coffee/coffee.pygments
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
This repository has been archived on 2024-06-20. You can view files and clone it, but you cannot make any changes to it's state, such as pushing and creating new issues, pull requests or comments.
coffee.pygments/tests/examplefiles/coq/coq_RelationClasses.output
Xia Li-yao 56f463e893
coq: Add some common keywords and improve recognition of Set and qualified identifiers (#2158) 
. is not an operator in Coq: in this specific usage, it is only meant to build a qualified name, so this rule really corresponds to a proper lexical rule in Coq

Unlike most languages, Coq has a large set of special words that are not reserved: they may still be used as identifiers. For example Prop is a special word, which currently gets highlighted as such in Equations.Prop.Equations, but it should be recognized as a regular name there. Because of how flexible the syntax of Coq is, it's not straightforward to disambiguate things with just a bunch of regexes, so we have to rely on heuristics. Skipping qualified names from being recognized as keywords is an easy win.
2022-06-11 15:41:14 +02:00

4535 lines
94 KiB
Text
Generated
Raw Permalink Blame History

'(*' Comment
' -' Comment
'*' Comment
'- coding: utf-8 -' Comment
'*' Comment
'- ' Comment
'*)' Comment
'\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n' Text
'(*' Comment
' v ' Comment
'*' Comment
' The Coq Proof Assistant / The Coq Development Team ' Comment
'*)' Comment
'\n' Text
'(*' Comment
' <O___,, ' Comment
'*' Comment
' INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 ' Comment
'*)' Comment
'\n' Text
'(*' Comment
' \\VV/ ' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n' Text
'(*' Comment
' // ' Comment
'*' Comment
' This file is distributed under the terms of the ' Comment
'*)' Comment
'\n' Text
'(*' Comment
' ' Comment
'*' Comment
' GNU Lesser General Public License Version 2.1 ' Comment
'*)' Comment
'\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'(*' Comment
'*' Comment
' ' Comment
'*' Comment
' Typeclass-based relations, tactics and standard instances\n\n This is the basic theory needed to formalize morphisms and setoids.\n\n Author: Matthieu Sozeau\n Institution: LRI, CNRS UMR 8623 - University Paris Sud\n' Comment
'*)' Comment
'\n\n' Text
'(*' Comment
' $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ ' Comment
'*)' Comment
'\n\n' Text
'Require' Keyword.Namespace
' ' Text
'Export' Keyword.Namespace
' ' Text
'Coq.Classes.Init' Name
'.' Operator
'\n' Text
'Require' Keyword.Namespace
' ' Text
'Import' Keyword.Namespace
' ' Text
'Coq.Program.Basics' Name
'.' Operator
'\n' Text
'Require' Keyword.Namespace
' ' Text
'Import' Keyword.Namespace
' ' Text
'Coq.Program.Tactics' Name
'.' Operator
'\n' Text
'Require' Keyword.Namespace
' ' Text
'Import' Keyword.Namespace
' ' Text
'Coq.Relations.Relation_Definitions' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We allow to unfold the [relation] definition while doing morphism search. ' Comment
'*)' Comment
'\n\n' Text
'Notation' Keyword.Namespace
' ' Text
'inverse' Name
' ' Text
'R' Name
' ' Text
':=' Operator
' ' Text
'(' Operator
'flip' Name
' ' Text
'(' Operator
'R' Name
':' Operator
'relation' Name
' ' Text
'_' Operator
')' Operator
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'_' Operator
')' Operator
'.' Operator
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'complement' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'=>' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'->' Operator
' ' Text
'False' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Opaque for proof-search. ' Comment
'*)' Comment
'\n' Text
'Typeclasses' Name
' ' Text
'Opaque' Name
' ' Text
'complement' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' These are convertible. ' Comment
'*)' Comment
'\n\n' Text
'Lemma' Keyword.Namespace
' ' Text
'complement_inverse' Name
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'A' Name
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
',' Operator
' ' Text
'complement' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'R' Name
')' Operator
' ' Text
'=' Operator
' ' Text
'inverse' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'reflexivity' Keyword.Pseudo
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We rebind relations in separate classes to be able to overload each proof. ' Comment
'*)' Comment
'\n\n' Text
'Set' Keyword.Namespace
' ' Text
'Implicit' Keyword.Namespace
' ' Text
'Arguments' Keyword.Namespace
'.' Operator
'\n' Text
'Unset' Keyword.Namespace
' ' Text
'Strict' Keyword.Namespace
' ' Text
'Implicit' Keyword.Namespace
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Reflexive' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'reflexivity' Keyword.Pseudo
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'x' Name
',' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'x' Name
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Irreflexive' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'irreflexivity' Name
' ' Text
':' Operator
' ' Text
'Reflexive' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'1' Literal.Number.Integer
' ' Text
'(' Operator
'Reflexive' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'@' Operator
'irreflexivity' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Symmetric' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'symmetry' Keyword
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
',' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'->' Operator
' ' Text
'R' Name
' ' Text
'y' Name
' ' Text
'x' Name
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Asymmetric' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'asymmetry' Name
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
',' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'->' Operator
' ' Text
'R' Name
' ' Text
'y' Name
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'False' Name
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Transitive' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'transitivity' Keyword
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'z' Name
',' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'->' Operator
' ' Text
'R' Name
' ' Text
'y' Name
' ' Text
'z' Name
' ' Text
'->' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'z' Name
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Resolve' Keyword.Namespace
' ' Text
'@' Operator
'irreflexivity' Name
' ' Text
':' Operator
' ' Text
'ord' Name
'.' Operator
'\n\n' Text
'Unset' Keyword.Namespace
' ' Text
'Implicit' Keyword.Namespace
' ' Text
'Arguments' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' A HintDb for relations. ' Comment
'*)' Comment
'\n\n' Text
'Ltac' Keyword.Namespace
' ' Text
'solve_relation' Name
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'goal' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'[' Operator
' ' Text
'|' Operator
'-' Operator
' ' Text
'?' Operator
'R' Name
' ' Text
'?' Operator
'x' Name
' ' Text
'?' Operator
'x' Name
' ' Text
']' Operator
' ' Text
'=>' Operator
' ' Text
'reflexivity' Keyword.Pseudo
'\n ' Text
'|' Operator
' ' Text
'[' Operator
' ' Text
'H' Name
' ' Text
':' Operator
' ' Text
'?' Operator
'R' Name
' ' Text
'?' Operator
'x' Name
' ' Text
'?' Operator
'y' Name
' ' Text
'|' Operator
'-' Operator
' ' Text
'?' Operator
'R' Name
' ' Text
'?' Operator
'y' Name
' ' Text
'?' Operator
'x' Name
' ' Text
']' Operator
' ' Text
'=>' Operator
' ' Text
'symmetry' Keyword
' ' Text
';' Operator
' ' Text
'exact' Keyword.Pseudo
' ' Text
'H' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'4' Literal.Number.Integer
' ' Text
'=>' Operator
' ' Text
'solve_relation' Name
' ' Text
':' Operator
' ' Text
'relations' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We can already dualize all these properties. ' Comment
'*)' Comment
'\n\n' Text
'Generalizable' Name
' ' Text
'Variables' Keyword.Namespace
' ' Text
'A' Name
' ' Text
'B' Name
' ' Text
'C' Name
' ' Text
'D' Name
' ' Text
'R' Name
' ' Text
'S' Name
' ' Text
'T' Name
' ' Text
'U' Name
' ' Text
'l' Name
' ' Text
'eqA' Name
' ' Text
'eqB' Name
' ' Text
'eqC' Name
' ' Text
'eqD' Name
'.' Operator
'\n\n' Text
'Lemma' Keyword.Namespace
' ' Text
'flip_Reflexive' Name
' ' Text
'`' Operator
'{' Operator
'Reflexive' Name
' ' Text
'A' Name
' ' Text
'R' Name
'}' Operator
' ' Text
':' Operator
' ' Text
'Reflexive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'tauto' Keyword
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Reflexive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'apply' Keyword
' ' Text
'flip_Reflexive' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Definition' Keyword.Namespace
' ' Text
'flip_Irreflexive' Name
' ' Text
'`' Operator
'(' Operator
'Irreflexive' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Irreflexive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'irreflexivity' Name
' ' Text
'(' Operator
'R' Name
':=' Operator
'R' Name
')' Operator
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Definition' Keyword.Namespace
' ' Text
'flip_Symmetric' Name
' ' Text
'`' Operator
'(' Operator
'Symmetric' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Symmetric' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'H' Name
' ' Text
'=>' Operator
' ' Text
'symmetry' Keyword
' ' Text
'(' Operator
'R' Name
':=' Operator
'R' Name
')' Operator
' ' Text
'H' Name
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Definition' Keyword.Namespace
' ' Text
'flip_Asymmetric' Name
' ' Text
'`' Operator
'(' Operator
'Asymmetric' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Asymmetric' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'H' Name
' ' Text
"H'" Name
' ' Text
'=>' Operator
' ' Text
'asymmetry' Name
' ' Text
'(' Operator
'R' Name
':=' Operator
'R' Name
')' Operator
' ' Text
'H' Name
' ' Text
"H'" Name
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Definition' Keyword.Namespace
' ' Text
'flip_Transitive' Name
' ' Text
'`' Operator
'(' Operator
'Transitive' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Transitive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'z' Name
' ' Text
'H' Name
' ' Text
"H'" Name
' ' Text
'=>' Operator
' ' Text
'transitivity' Keyword
' ' Text
'(' Operator
'R' Name
':=' Operator
'R' Name
')' Operator
' ' Text
"H'" Name
' ' Text
'H' Name
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Irreflexive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'flip_Irreflexive' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Symmetric' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'flip_Symmetric' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Asymmetric' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'flip_Asymmetric' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Transitive' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'flip_Transitive' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'Reflexive_complement_Irreflexive' Name
' ' Text
'`' Operator
'(' Operator
'Reflexive' Name
' ' Text
'A' Name
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Irreflexive' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'complement_Symmetric' Name
' ' Text
'`' Operator
'(' Operator
'Symmetric' Name
' ' Text
'A' Name
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
')' Operator
' ' Text
':' Operator
' ' Text
'Symmetric' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Symmetric' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'complement_Symmetric' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'Irreflexive' Name
' ' Text
'(' Operator
'complement' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'Reflexive_complement_Irreflexive' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' ' Comment
'*' Comment
' Standard instances. ' Comment
'*)' Comment
'\n\n' Text
'Ltac' Keyword.Namespace
' ' Text
'reduce_hyp' Name
' ' Text
'H' Name
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'type' Name
' ' Text
'of' Keyword
' ' Text
'H' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'context' Name
' ' Text
'[' Operator
' ' Text
'_' Operator
' ' Text
'<->' Operator
' ' Text
'_' Operator
' ' Text
']' Operator
' ' Text
'=>' Operator
' ' Text
'fail' Name
' ' Text
'1' Literal.Number.Integer
'\n ' Text
'|' Operator
' ' Text
'_' Operator
' ' Text
'=>' Operator
' ' Text
'red' Keyword
' ' Text
'in' Keyword
' ' Text
'H' Name
' ' Text
';' Operator
' ' Text
'try' Keyword.Reserved
' ' Text
'reduce_hyp' Name
' ' Text
'H' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Ltac' Keyword.Namespace
' ' Text
'reduce_goal' Name
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'goal' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'[' Operator
' ' Text
'|' Operator
'-' Operator
' ' Text
'_' Operator
' ' Text
'<->' Operator
' ' Text
'_' Operator
' ' Text
']' Operator
' ' Text
'=>' Operator
' ' Text
'fail' Name
' ' Text
'1' Literal.Number.Integer
'\n ' Text
'|' Operator
' ' Text
'_' Operator
' ' Text
'=>' Operator
' ' Text
'red' Keyword
' ' Text
';' Operator
' ' Text
'intros' Keyword
' ' Text
';' Operator
' ' Text
'try' Keyword.Reserved
' ' Text
'reduce_goal' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Tactic' Keyword.Namespace
' ' Text
'Notation' Keyword.Namespace
' ' Text
'"' Literal.String.Double
'reduce' Literal.String.Double
'"' Literal.String.Double
' ' Text
'"' Literal.String.Double
'in' Literal.String.Double
'"' Literal.String.Double
' ' Text
'hyp' Name
'(' Operator
'Hid' Name
')' Operator
' ' Text
':=' Operator
' ' Text
'reduce_hyp' Name
' ' Text
'Hid' Name
'.' Operator
'\n\n' Text
'Ltac' Keyword.Namespace
' ' Text
'reduce' Name
' ' Text
':=' Operator
' ' Text
'reduce_goal' Name
'.' Operator
'\n\n' Text
'Tactic' Keyword.Namespace
' ' Text
'Notation' Keyword.Namespace
' ' Text
'"' Literal.String.Double
'apply' Literal.String.Double
'"' Literal.String.Double
' ' Text
'"' Literal.String.Double
'*' Literal.String.Double
'"' Literal.String.Double
' ' Text
'constr' Name
'(' Operator
't' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'first' Keyword.Reserved
' ' Text
'[' Operator
' ' Text
'refine' Keyword
' ' Text
't' Name
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
'\n ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
'|' Operator
' ' Text
'refine' Keyword
' ' Text
'(' Operator
't' Name
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
' ' Text
'_' Operator
')' Operator
' ' Text
']' Operator
'.' Operator
'\n\n' Text
'Ltac' Keyword.Namespace
' ' Text
'simpl_relation' Name
' ' Text
':=' Operator
'\n ' Text
'unfold' Keyword
' ' Text
'flip' Name
',' Operator
' ' Text
'impl' Name
',' Operator
' ' Text
'arrow' Name
' ' Text
';' Operator
' ' Text
'try' Keyword.Reserved
' ' Text
'reduce' Name
' ' Text
';' Operator
' ' Text
'program_simpl' Name
' ' Text
';' Operator
'\n ' Text
'try' Keyword.Reserved
' ' Text
'(' Operator
' ' Text
'solve' Keyword.Pseudo
' ' Text
'[' Operator
' ' Text
'intuition' Keyword
' ' Text
']' Operator
')' Operator
'.' Operator
'\n\n' Text
'Local' Keyword.Namespace
' ' Text
'Obligation' Name
' ' Text
'Tactic' Keyword.Namespace
' ' Text
':=' Operator
' ' Text
'simpl_relation' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Logical implication. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'impl_Reflexive' Name
' ' Text
':' Operator
' ' Text
'Reflexive' Name
' ' Text
'impl' Name
'.' Operator
'\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'impl_Transitive' Name
' ' Text
':' Operator
' ' Text
'Transitive' Name
' ' Text
'impl' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Logical equivalence. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'iff_Reflexive' Name
' ' Text
':' Operator
' ' Text
'Reflexive' Name
' ' Text
'iff' Name
'.' Operator
'\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'iff_Symmetric' Name
' ' Text
':' Operator
' ' Text
'Symmetric' Name
' ' Text
'iff' Name
'.' Operator
'\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'iff_Transitive' Name
' ' Text
':' Operator
' ' Text
'Transitive' Name
' ' Text
'iff' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Leibniz equality. ' Comment
'*)' Comment
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'eq_Reflexive' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
':' Operator
' ' Text
'Reflexive' Name
' ' Text
'(' Operator
'@' Operator
'eq' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
' ' Text
'@' Operator
'eq_refl' Name
' ' Text
'A' Name
'.' Operator
'\n' Text
'Instance' Keyword.Namespace
' ' Text
'eq_Symmetric' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
':' Operator
' ' Text
'Symmetric' Name
' ' Text
'(' Operator
'@' Operator
'eq' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
' ' Text
'@' Operator
'eq_sym' Name
' ' Text
'A' Name
'.' Operator
'\n' Text
'Instance' Keyword.Namespace
' ' Text
'eq_Transitive' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
':' Operator
' ' Text
'Transitive' Name
' ' Text
'(' Operator
'@' Operator
'eq' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
' ' Text
'@' Operator
'eq_trans' Name
' ' Text
'A' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Various combinations of reflexivity, symmetry and transitivity. ' Comment
'*)' Comment
'\n\n' Text
'(*' Comment
'*' Comment
' A [PreOrder] is both Reflexive and Transitive. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'PreOrder' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
' ' Text
'{' Operator
'\n ' Text
'PreOrder_Reflexive' Name
' ' Text
':>' Operator
' ' Text
'Reflexive' Name
' ' Text
'R' Name
' ' Text
';' Operator
'\n ' Text
'PreOrder_Transitive' Name
' ' Text
':>' Operator
' ' Text
'Transitive' Name
' ' Text
'R' Name
' ' Text
'}' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' A partial equivalence relation is Symmetric and Transitive. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'PER' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
' ' Text
'{' Operator
'\n ' Text
'PER_Symmetric' Name
' ' Text
':>' Operator
' ' Text
'Symmetric' Name
' ' Text
'R' Name
' ' Text
';' Operator
'\n ' Text
'PER_Transitive' Name
' ' Text
':>' Operator
' ' Text
'Transitive' Name
' ' Text
'R' Name
' ' Text
'}' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Equivalence relations. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Equivalence' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
' ' Text
'{' Operator
'\n ' Text
'Equivalence_Reflexive' Name
' ' Text
':>' Operator
' ' Text
'Reflexive' Name
' ' Text
'R' Name
' ' Text
';' Operator
'\n ' Text
'Equivalence_Symmetric' Name
' ' Text
':>' Operator
' ' Text
'Symmetric' Name
' ' Text
'R' Name
' ' Text
';' Operator
'\n ' Text
'Equivalence_Transitive' Name
' ' Text
':>' Operator
' ' Text
'Transitive' Name
' ' Text
'R' Name
' ' Text
'}' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' An Equivalence is a PER plus reflexivity. ' Comment
'*)' Comment
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'Equivalence_PER' Name
' ' Text
'`' Operator
'(' Operator
'Equivalence' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'PER' Name
' ' Text
'R' Name
' ' Text
'|' Operator
' ' Text
'10' Literal.Number.Integer
' ' Text
':=' Operator
'\n ' Text
'{' Operator
' ' Text
'PER_Symmetric' Name
' ' Text
':=' Operator
' ' Text
'Equivalence_Symmetric' Name
' ' Text
';' Operator
'\n ' Text
'PER_Transitive' Name
' ' Text
':=' Operator
' ' Text
'Equivalence_Transitive' Name
' ' Text
'}' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We can now define antisymmetry w.r.t. an equivalence relation on the carrier. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'Antisymmetric' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'`' Operator
'{' Operator
'equ' Name
' ' Text
':' Operator
' ' Text
'Equivalence' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'antisymmetry' Name
' ' Text
':' Operator
' ' Text
'forall' Keyword
' ' Text
'{' Operator
'x' Name
' ' Text
'y' Name
'}' Operator
',' Operator
' ' Text
'R' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'->' Operator
' ' Text
'R' Name
' ' Text
'y' Name
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'eqA' Name
' ' Text
'x' Name
' ' Text
'y' Name
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Definition' Keyword.Namespace
' ' Text
'flip_antiSymmetric' Name
' ' Text
'`' Operator
'(' Operator
'Antisymmetric' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
'\n ' Text
'Antisymmetric' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'(' Operator
'flip' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Leibinz equality [eq] is an equivalence relation.\n The instance has low priority as it is always applicable\n if only the type is constrained. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'eq_equivalence' Name
' ' Text
':' Operator
' ' Text
'Equivalence' Name
' ' Text
'(' Operator
'@' Operator
'eq' Name
' ' Text
'A' Name
')' Operator
' ' Text
'|' Operator
' ' Text
'10' Literal.Number.Integer
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Logical equivalence [iff] is an equivalence relation. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'iff_equivalence' Name
' ' Text
':' Operator
' ' Text
'Equivalence' Name
' ' Text
'iff' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We now develop a generalization of results on relations for arbitrary predicates.\n The resulting theory can be applied to homogeneous binary relations but also to\n arbitrary n-ary predicates. ' Comment
'*)' Comment
'\n\n' Text
'Local' Keyword.Namespace
' ' Text
'Open' Keyword.Namespace
' ' Text
'Scope' Keyword.Namespace
' ' Text
'list_scope' Name
'.' Operator
'\n\n' Text
'(*' Comment
' Notation " [ ] " := nil : list_scope. ' Comment
'*)' Comment
'\n' Text
'(*' Comment
' Notation " [ x ; .. ; y ] " := ' Comment
'(' Comment
'cons x .. ' Comment
'(' Comment
'cons y nil' Comment
')' Comment
' ..' Comment
')' Comment
' ' Comment
'(' Comment
'at level 1' Comment
')' Comment
' : list_scope. ' Comment
'*)' Comment
'\n\n' Text
'(*' Comment
'*' Comment
' A compact representation of non-dependent arities, with the codomain singled-out. ' Comment
'*)' Comment
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'arrows' Name
' ' Text
'(' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
'(' Operator
'r' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'r' Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
"l'" Name
' ' Text
'=>' Operator
' ' Text
'A' Name
' ' Text
'->' Operator
' ' Text
'arrows' Name
' ' Text
"l'" Name
' ' Text
'r' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We can define abbreviations for operation and relation types based on [arrows]. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'unary_operation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'arrows' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'A' Name
'.' Operator
'\n' Text
'Definition' Keyword.Namespace
' ' Text
'binary_operation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'arrows' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'A' Name
'.' Operator
'\n' Text
'Definition' Keyword.Namespace
' ' Text
'ternary_operation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'arrows' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'A' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We define n-ary [predicate]s as functions into [Prop]. ' Comment
'*)' Comment
'\n\n' Text
'Notation' Keyword.Namespace
' ' Text
'predicate' Name
' ' Text
'l' Name
' ' Text
':=' Operator
' ' Text
'(' Operator
'arrows' Name
' ' Text
'l' Name
' ' Text
'Prop' Keyword.Type
')' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Unary predicates, or sets. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'unary_predicate' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'predicate' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Homogeneous binary relations, equivalent to [relation A]. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'binary_relation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
' ' Text
'predicate' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We can close a predicate by universal or existential quantification. ' Comment
'*)' Comment
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'predicate_all' Name
' ' Text
'(' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
' ' Text
'predicate' Name
' ' Text
'l' Name
' ' Text
'->' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'f' Name
' ' Text
'=>' Operator
' ' Text
'f' Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'f' Name
' ' Text
'=>' Operator
' ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
':' Operator
' ' Text
'A' Name
',' Operator
' ' Text
'predicate_all' Name
' ' Text
'tl' Name
' ' Text
'(' Operator
'f' Name
' ' Text
'x' Name
')' Operator
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'predicate_exists' Name
' ' Text
'(' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
' ' Text
'predicate' Name
' ' Text
'l' Name
' ' Text
'->' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'f' Name
' ' Text
'=>' Operator
' ' Text
'f' Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'f' Name
' ' Text
'=>' Operator
' ' Text
'exists' Keyword
' ' Text
'x' Name
' ' Text
':' Operator
' ' Text
'A' Name
',' Operator
' ' Text
'predicate_exists' Name
' ' Text
'tl' Name
' ' Text
'(' Operator
'f' Name
' ' Text
'x' Name
')' Operator
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Pointwise extension of a binary operation on [T] to a binary operation\n on functions whose codomain is [T].\n For an operator on [Prop] this lifts the operator to a binary operation. ' Comment
'*)' Comment
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'pointwise_extension' Name
' ' Text
'{' Operator
'T' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
'(' Operator
'op' Name
' ' Text
':' Operator
' ' Text
'binary_operation' Name
' ' Text
'T' Name
')' Operator
'\n ' Text
'(' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
' ' Text
'binary_operation' Name
' ' Text
'(' Operator
'arrows' Name
' ' Text
'l' Name
' ' Text
'T' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'R' Name
' ' Text
"R'" Name
' ' Text
'=>' Operator
' ' Text
'op' Name
' ' Text
'R' Name
' ' Text
"R'" Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'R' Name
' ' Text
"R'" Name
' ' Text
'=>' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'=>' Operator
' ' Text
'pointwise_extension' Name
' ' Text
'op' Name
' ' Text
'tl' Name
' ' Text
'(' Operator
'R' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
"R'" Name
' ' Text
'x' Name
')' Operator
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. ' Comment
'*)' Comment
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'pointwise_lifting' Name
' ' Text
'(' Operator
'op' Name
' ' Text
':' Operator
' ' Text
'binary_relation' Name
' ' Text
'Prop' Keyword.Type
')' Operator
' ' Text
'(' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
' ' Text
'binary_relation' Name
' ' Text
'(' Operator
'predicate' Name
' ' Text
'l' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'R' Name
' ' Text
"R'" Name
' ' Text
'=>' Operator
' ' Text
'op' Name
' ' Text
'R' Name
' ' Text
"R'" Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'R' Name
' ' Text
"R'" Name
' ' Text
'=>' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
',' Operator
' ' Text
'pointwise_lifting' Name
' ' Text
'op' Name
' ' Text
'tl' Name
' ' Text
'(' Operator
'R' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
"R'" Name
' ' Text
'x' Name
')' Operator
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'predicate_equivalence' Name
' ' Text
'{' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
':' Operator
' ' Text
'binary_relation' Name
' ' Text
'(' Operator
'predicate' Name
' ' Text
'l' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'pointwise_lifting' Name
' ' Text
'iff' Name
' ' Text
'l' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The n-ary implication relation, defined by lifting the 0-ary [impl] relation. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'predicate_implication' Name
' ' Text
'{' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
':=' Operator
'\n ' Text
'pointwise_lifting' Name
' ' Text
'impl' Name
' ' Text
'l' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Notations for pointwise equivalence and implication of predicates. ' Comment
'*)' Comment
'\n\n' Text
'Infix' Name
' ' Text
'"' Literal.String.Double
'<∙>' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'predicate_equivalence' Name
' ' Text
'(' Operator
'at' Name
' ' Text
'level' Name
' ' Text
'95' Literal.Number.Integer
',' Operator
' ' Text
'no' Name
' ' Text
'associativity' Name
')' Operator
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n' Text
'Infix' Name
' ' Text
'"' Literal.String.Double
'-∙>' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'predicate_implication' Name
' ' Text
'(' Operator
'at' Name
' ' Text
'level' Name
' ' Text
'70' Literal.Number.Integer
',' Operator
' ' Text
'right' Keyword
' ' Text
'associativity' Name
')' Operator
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n\n' Text
'Open' Keyword.Namespace
' ' Text
'Local' Keyword.Namespace
' ' Text
'Scope' Keyword.Namespace
' ' Text
'predicate_scope' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The pointwise liftings of conjunction and disjunctions.\n Note that these are [binary_operation]s, building new relations out of old ones. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'predicate_intersection' Name
' ' Text
':=' Operator
' ' Text
'pointwise_extension' Name
' ' Text
'and' Name
'.' Operator
'\n' Text
'Definition' Keyword.Namespace
' ' Text
'predicate_union' Name
' ' Text
':=' Operator
' ' Text
'pointwise_extension' Name
' ' Text
'or' Name
'.' Operator
'\n\n' Text
'Infix' Name
' ' Text
'"' Literal.String.Double
'/∙\\' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'predicate_intersection' Name
' ' Text
'(' Operator
'at' Name
' ' Text
'level' Name
' ' Text
'80' Literal.Number.Integer
',' Operator
' ' Text
'right' Keyword
' ' Text
'associativity' Name
')' Operator
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n' Text
'Infix' Name
' ' Text
'"' Literal.String.Double
'\\∙/' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'predicate_union' Name
' ' Text
'(' Operator
'at' Name
' ' Text
'level' Name
' ' Text
'85' Literal.Number.Integer
',' Operator
' ' Text
'right' Keyword
' ' Text
'associativity' Name
')' Operator
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The always [True] and always [False] predicates. ' Comment
'*)' Comment
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'true' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
'{' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
':' Operator
' ' Text
'predicate' Name
' ' Text
'l' Name
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'True' Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'_' Operator
' ' Text
'=>' Operator
' ' Text
'@' Operator
'true' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
'tl' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Fixpoint' Keyword.Namespace
' ' Text
'false' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
'{' Operator
'l' Name
' ' Text
':' Operator
' ' Text
'list' Name
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
':' Operator
' ' Text
'predicate' Name
' ' Text
'l' Name
' ' Text
':=' Operator
'\n ' Text
'match' Keyword
' ' Text
'l' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'nil' Name
' ' Text
'=>' Operator
' ' Text
'False' Name
'\n ' Text
'|' Operator
' ' Text
'A' Name
' ' Text
'::' Operator
' ' Text
'tl' Name
' ' Text
'=>' Operator
' ' Text
'fun' Keyword
' ' Text
'_' Operator
' ' Text
'=>' Operator
' ' Text
'@' Operator
'false' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
'tl' Name
'\n ' Text
'end' Keyword
'.' Operator
'\n\n' Text
'Notation' Keyword.Namespace
' ' Text
'"' Literal.String.Double
'∙⊤∙' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'true' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n' Text
'Notation' Keyword.Namespace
' ' Text
'"' Literal.String.Double
'∙⊥∙' Literal.String.Double
'"' Literal.String.Double
' ' Text
':=' Operator
' ' Text
'false' Name.Builtin.Pseudo
'_' Operator
'predicate' Name
' ' Text
':' Operator
' ' Text
'predicate_scope' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Predicate equivalence is an equivalence, and predicate implication defines a preorder. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'predicate_equivalence_equivalence' Name
' ' Text
':' Operator
' ' Text
'Equivalence' Name
' ' Text
'(' Operator
'@' Operator
'predicate_equivalence' Name
' ' Text
'l' Name
')' Operator
'.' Operator
'\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'induction' Keyword
' ' Text
'l' Name
' ' Text
';' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'induction' Keyword
' ' Text
'l' Name
' ' Text
';' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'fold' Keyword
' ' Text
'pointwise_lifting' Name
'.' Operator
'\n ' Text
'induction' Keyword
' ' Text
'l' Name
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'intros' Keyword
'.' Operator
' ' Text
'simpl' Keyword
' ' Text
'in' Keyword
' ' Text
'*' Operator
'.' Operator
' ' Text
'pose' Keyword
' ' Text
'(' Operator
'IHl' Name
' ' Text
'(' Operator
'x' Name
' ' Text
'x0' Name
')' Operator
' ' Text
'(' Operator
'y' Name
' ' Text
'x0' Name
')' Operator
' ' Text
'(' Operator
'z' Name
' ' Text
'x0' Name
')' Operator
')' Operator
'.' Operator
'\n ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'predicate_implication_preorder' Name
' ' Text
':' Operator
'\n ' Text
'PreOrder' Name
' ' Text
'(' Operator
'@' Operator
'predicate_implication' Name
' ' Text
'l' Name
')' Operator
'.' Operator
'\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'induction' Keyword
' ' Text
'l' Name
' ' Text
';' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'induction' Keyword
' ' Text
'l' Name
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'unfold' Keyword
' ' Text
'predicate_implication' Name
' ' Text
'in' Keyword
' ' Text
'*' Operator
'.' Operator
' ' Text
'simpl' Keyword
' ' Text
'in' Keyword
' ' Text
'*' Operator
'.' Operator
'\n ' Text
'intro' Keyword
'.' Operator
' ' Text
'pose' Keyword
' ' Text
'(' Operator
'IHl' Name
' ' Text
'(' Operator
'x' Name
' ' Text
'x0' Name
')' Operator
' ' Text
'(' Operator
'y' Name
' ' Text
'x0' Name
')' Operator
' ' Text
'(' Operator
'z' Name
' ' Text
'x0' Name
')' Operator
')' Operator
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' We define the various operations which define the algebra on binary relations,\n from the general ones. ' Comment
'*)' Comment
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'relation_equivalence' Name
' ' Text
'{' Operator
'A' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'(' Operator
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
'\n ' Text
'@' Operator
'predicate_equivalence' Name
' ' Text
'(' Operator
'_' Operator
'::' Operator
'_' Operator
'::' Operator
'nil' Name
')' Operator
'.' Operator
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'subrelation' Name
' ' Text
'{' Operator
'A' Name
':' Operator
'Type' Keyword.Type
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
"R'" Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Prop' Keyword.Type
' ' Text
':=' Operator
'\n ' Text
'is_subrelation' Name
' ' Text
':' Operator
' ' Text
'@' Operator
'predicate_implication' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'R' Name
' ' Text
"R'" Name
'.' Operator
'\n\n' Text
'Implicit' Keyword.Namespace
' ' Text
'Arguments' Keyword.Namespace
' ' Text
'subrelation' Name
' ' Text
'[' Operator
'[' Operator
'A' Name
']' Operator
']' Operator
'.' Operator
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'relation_conjunction' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
'(' Operator
"R'" Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
'\n ' Text
'@' Operator
'predicate_intersection' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'R' Name
' ' Text
"R'" Name
'.' Operator
'\n\n' Text
'Definition' Keyword.Namespace
' ' Text
'relation_disjunction' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
'(' Operator
"R'" Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
' ' Text
':=' Operator
'\n ' Text
'@' Operator
'predicate_union' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
' ' Text
'R' Name
' ' Text
"R'" Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Relation equivalence is an equivalence, and subrelation defines a partial order. ' Comment
'*)' Comment
'\n\n' Text
'Set' Keyword.Namespace
' ' Text
'Automatic' Name
' ' Text
'Introduction' Name
'.' Operator
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'relation_equivalence_equivalence' Name
' ' Text
'(' Operator
'A' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
')' Operator
' ' Text
':' Operator
'\n ' Text
'Equivalence' Name
' ' Text
'(' Operator
'@' Operator
'relation_equivalence' Name
' ' Text
'A' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'exact' Keyword.Pseudo
' ' Text
'(' Operator
'@' Operator
'predicate_equivalence_equivalence' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
')' Operator
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'relation_implication_preorder' Name
' ' Text
'A' Name
' ' Text
':' Operator
' ' Text
'PreOrder' Name
' ' Text
'(' Operator
'@' Operator
'subrelation' Name
' ' Text
'A' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'exact' Keyword.Pseudo
' ' Text
'(' Operator
'@' Operator
'predicate_implication_preorder' Name
' ' Text
'(' Operator
'A' Name
'::' Operator
'A' Name
'::' Operator
'nil' Name
')' Operator
')' Operator
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' ' Comment
'*' Comment
'*' Comment
'*' Comment
' Partial Order.\n A partial order is a preorder which is additionally antisymmetric.\n We give an equivalent definition, up-to an equivalence relation\n on the carrier. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'PartialOrder' Name
' ' Text
'{' Operator
'A' Name
'}' Operator
' ' Text
'eqA' Name
' ' Text
'`' Operator
'{' Operator
'equ' Name
' ' Text
':' Operator
' ' Text
'Equivalence' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
'}' Operator
' ' Text
'R' Name
' ' Text
'`' Operator
'{' Operator
'preo' Name
' ' Text
':' Operator
' ' Text
'PreOrder' Name
' ' Text
'A' Name
' ' Text
'R' Name
'}' Operator
' ' Text
':=' Operator
'\n ' Text
'partial_order_equivalence' Name
' ' Text
':' Operator
' ' Text
'relation_equivalence' Name
' ' Text
'eqA' Name
' ' Text
'(' Operator
'relation_conjunction' Name
' ' Text
'R' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'R' Name
')' Operator
')' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The equivalence proof is sufficient for proving that [R] must be a morphism\n for equivalence ' Comment
'(' Comment
'see Morphisms' Comment
')' Comment
'.\n It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] ' Comment
'*)' Comment
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'partial_order_antisym' Name
' ' Text
'`' Operator
'(' Operator
'PartialOrder' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'!' Operator
' ' Text
'Antisymmetric' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'R' Name
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
' ' Text
'with' Keyword
' ' Text
'auto' Keyword
'.' Operator
'\n ' Text
'reduce_goal' Name
'.' Operator
'\n ' Text
'pose' Keyword
' ' Text
'proof' Name
' ' Text
'partial_order_equivalence' Name
' ' Text
'as' Keyword
' ' Text
'poe' Name
'.' Operator
' ' Text
'do' Keyword.Reserved
' ' Text
'3' Literal.Number.Integer
' ' Text
'red' Keyword
' ' Text
'in' Keyword
' ' Text
'poe' Name
'.' Operator
'\n ' Text
'apply' Keyword
' ' Text
'<-' Operator
' ' Text
'poe' Name
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' The partial order defined by subrelation and relation equivalence. ' Comment
'*)' Comment
'\n\n' Text
'Program' Name
' ' Text
'Instance' Keyword.Namespace
' ' Text
'subrelation_partial_order' Name
' ' Text
':' Operator
'\n ' Text
'!' Operator
' ' Text
'PartialOrder' Name
' ' Text
'(' Operator
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
'relation_equivalence' Name
' ' Text
'subrelation' Name
'.' Operator
'\n\n ' Text
'Next' Name
' ' Text
'Obligation' Name
'.' Operator
'\n ' Text
'Proof' Keyword.Namespace
'.' Operator
'\n ' Text
'unfold' Keyword
' ' Text
'relation_equivalence' Name
' ' Text
'in' Keyword
' ' Text
'*' Operator
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
'\n ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Typeclasses' Name
' ' Text
'Opaque' Name
' ' Text
'arrows' Name
' ' Text
'predicate_implication' Name
' ' Text
'predicate_equivalence' Name
'\n ' Text
'relation_equivalence' Name
' ' Text
'pointwise_lifting' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Rewrite relation on a given support: declares a relation as a rewrite\n relation for use by the generalized rewriting tactic.\n It helps choosing if a rewrite should be handled\n by the generalized or the regular rewriting tactic using leibniz equality.\n Users can declare an [RewriteRelation A RA] anywhere to declare default\n relations. This is also done automatically by the [Declare Relation A RA]\n commands. ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'RewriteRelation' Name
' ' Text
'{' Operator
'A' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
'(' Operator
'RA' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
'.' Operator
'\n\n' Text
'Instance' Keyword.Namespace
':' Operator
' ' Text
'RewriteRelation' Name
' ' Text
'impl' Name
'.' Operator
'\n' Text
'Instance' Keyword.Namespace
':' Operator
' ' Text
'RewriteRelation' Name
' ' Text
'iff' Name
'.' Operator
'\n' Text
'Instance' Keyword.Namespace
':' Operator
' ' Text
'RewriteRelation' Name
' ' Text
'(' Operator
'@' Operator
'relation_equivalence' Name
' ' Text
'A' Name
')' Operator
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Any [Equivalence] declared in the context is automatically considered\n a rewrite relation. ' Comment
'*)' Comment
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'equivalence_rewrite_relation' Name
' ' Text
'`' Operator
'(' Operator
'Equivalence' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
')' Operator
' ' Text
':' Operator
' ' Text
'RewriteRelation' Name
' ' Text
'eqA' Name
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Strict Order ' Comment
'*)' Comment
'\n\n' Text
'Class' Keyword.Namespace
' ' Text
'StrictOrder' Name
' ' Text
'{' Operator
'A' Name
' ' Text
':' Operator
' ' Text
'Type' Keyword.Type
'}' Operator
' ' Text
'(' Operator
'R' Name
' ' Text
':' Operator
' ' Text
'relation' Name
' ' Text
'A' Name
')' Operator
' ' Text
':=' Operator
' ' Text
'{' Operator
'\n ' Text
'StrictOrder_Irreflexive' Name
' ' Text
':>' Operator
' ' Text
'Irreflexive' Name
' ' Text
'R' Name
' ' Text
';' Operator
'\n ' Text
'StrictOrder_Transitive' Name
' ' Text
':>' Operator
' ' Text
'Transitive' Name
' ' Text
'R' Name
'\n' Text
'}' Operator
'.' Operator
'\n\n' Text
'Instance' Keyword.Namespace
' ' Text
'StrictOrder_Asymmetric' Name
' ' Text
'`' Operator
'(' Operator
'StrictOrder' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'Asymmetric' Name
' ' Text
'R' Name
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Inversing a [StrictOrder] gives another [StrictOrder] ' Comment
'*)' Comment
'\n\n' Text
'Lemma' Keyword.Namespace
' ' Text
'StrictOrder_inverse' Name
' ' Text
'`' Operator
'(' Operator
'StrictOrder' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'StrictOrder' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'(*' Comment
'*' Comment
' Same for [PartialOrder]. ' Comment
'*)' Comment
'\n\n' Text
'Lemma' Keyword.Namespace
' ' Text
'PreOrder_inverse' Name
' ' Text
'`' Operator
'(' Operator
'PreOrder' Name
' ' Text
'A' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'PreOrder' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'StrictOrder' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'StrictOrder_inverse' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'PreOrder' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'PreOrder_inverse' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n\n' Text
'Lemma' Keyword.Namespace
' ' Text
'PartialOrder_inverse' Name
' ' Text
'`' Operator
'(' Operator
'PartialOrder' Name
' ' Text
'A' Name
' ' Text
'eqA' Name
' ' Text
'R' Name
')' Operator
' ' Text
':' Operator
' ' Text
'PartialOrder' Name
' ' Text
'eqA' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'R' Name
')' Operator
'.' Operator
'\n' Text
'Proof' Keyword.Namespace
'.' Operator
' ' Text
'firstorder' Name
'.' Operator
' ' Text
'Qed' Keyword.Namespace
'.' Operator
'\n\n' Text
'Hint' Keyword.Namespace
' ' Text
'Extern' Name
' ' Text
'3' Literal.Number.Integer
' ' Text
'(' Operator
'PartialOrder' Name
' ' Text
'(' Operator
'inverse' Name
' ' Text
'_' Operator
')' Operator
')' Operator
' ' Text
'=>' Operator
' ' Text
'class_apply' Name
' ' Text
'PartialOrder_inverse' Name
' ' Text
':' Operator
' ' Text
'typeclass_instances' Name
'.' Operator
'\n' Text
Reference in a new issue View git blame Copy permalink