reference documentation

Article word-witness.art

path: "vendor/opentheory/data/theories/word-witness/word-witness.art"

316 bytes
"Data.Word.width"
"Number.Natural.zero"
const
"Number.Natural.natural"
typeOp
nil
opType
0
def
constTerm
defineConst
pop
0
ref
constTerm
1
def
refl
nil
"="
const
"->"
typeOp
2
def
0
ref
2
remove
0
remove
"bool"
typeOp
nil
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
1
ref
appTerm
1
remove
appTerm
thm