Skip to content

S
smglom
Commit a5ce8e19 authored by Dennis Müller's avatar Dennis Müller
Browse files
Options

notations

parent 49ce7357
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
source/graphs/graphs.mmt
View file @ a5ce8e19
......@@ -22,8 +22,8 @@ theory Graphs : base:?Logic =
include ts:?RelationClosure ❙
nodesOf : {g: dgraph}set (g.nodetype) ❘ = [g] (g.nodes) ❘ # nodes 1❙
dEdgesOf : {g: dgraph}relOn (g.nodetype) ❘ = [g] (g.edges) ❘ # edges 1❙
uEdgesOf : {g: ugraph}relOn (g.nodetype) ❘ = [g] symmetric_closure (g.edges) ❘ # edges 1 ❙
dEdgesOf : {g: dgraph}relOn (g.nodetype) ❘ = [g] (g.edges) ❘ # edgesOf 1❙
uEdgesOf : {g: ugraph}relOn (g.nodetype) ❘ = [g] symmetric_closure (g.edges) ❘ # edgesOf 1 ❙
include base:?InformalProofs ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment