Library/TermNet.hs


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

module Library.TermNet(
	TermNet,
	empty,
	addThm
	) where


import Library.ProofGraph
import Library.Object
import Library.Theorem


data TermNet = Empty | Leaf Object Node | Branch String [TermNet]


empty :: TermNet
empty = Empty


addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
addThm net graph node =