| : | %language ElabReflection
addTypeDecl : Elab ()
addTypeDecl = do
let tname : TTName = `{{GenData}}
declareDatatype $ Declare tname [] RType
defineDatatype $ DefineDatatype tname []
%runElab addTypeDecl |
|
After each tactic we will look at the state:
| We start with the type signature like this: | %language ElabReflection
addTypeDecl : Elab ()
addTypeDecl = do
let tname : TTName = `{{GenData}} |
| In order to investigate how the program works we can look at the proofState at each stage as the tactics are applied. So here is the proofState at the start: |  |
| We can also look at the logic at each stage: |  |
| The term is: | |
getEnv getGoal getHoles |
x |
| getGuess | error no guess |
|
x |
| x | declareDatatype $ Declare tname [] RType |
 |
|
 |
|
| Term: | ? {hole_0} . {hole_0} |
getEnv getGoal getHoles |
getEnv=[] |
| getGuess | x |
Holes:
----------------------------------
{hole_0} : Language.Reflection.Elab.Elab Unit |
|
| Place a term into a hole, unifying its type | defineDatatype $ DefineDatatype tname [] |
 |
|
 |
|
| Term: | ? {hole_0} . {hole_0} |
getEnv getGoal getHoles |
getEnv=[] |
| getGuess | x |
Holes:
----------------------------------
{hole_0} : Language.Reflection.Elab.Elab Unit |
|
x |
|
 |
|
x |
|
getEnv getGoal getHoles |
x |
| getGuess | x |
x |
