Thms
nfa
1
Sections
AutomataTheory
Doc
NOTE:
This operator coercing a
to a Prop is normally invisible since it is pretty obvious when it is needed.
assert
Def
b == if b
True else False fi
Thm*
b:
. b
Prop
About:
b == if b
True else False fi
b:
. b 
Prop to a Prop is normally invisible since it is pretty obvious when it is
needed.
b == if b True else False fi
