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