| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
T2A.Core
- data AgdaSignature
- buildSignature :: ProofMap -> String -> Maybe AgdaSignature
- fname :: AgdaSignature -> String
Documentation
data AgdaSignature
An
Agda
type signature α : τ
Constructors
| Signature String [Formula] | Regular top level signature |
| ScopedSignature String [Formula] | Fully scoped signature with no newly introduced type variables |
Instances
buildSignature :: ProofMap -> String -> Maybe AgdaSignature
Given a proof map ω and some formula name φ, construct
the appropriated AgdaSignature based on the parents of φ
fname :: AgdaSignature -> String
Retrieve signature name