You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
One of the main goals of the project is to have a backend for Agda proper that uses Agda Core to type-check the elaborated internal syntax of a module. Steps that we need to take to get this to work:
Implement the translation from Agda Terms to Agda Core Terms.
Implement a translation from an Agda Signature to an Agda Core GlobalScope + Signature for it.
Implement a translation from Agda's CompiledClauses to an Agda Core Term using TCases for each node in the case tree.
Implement the actual backend functionality that calls the typechecker on each term in a definition.
Add test cases
The text was updated successfully, but these errors were encountered:
One of the main goals of the project is to have a backend for Agda proper that uses Agda Core to type-check the elaborated internal syntax of a module. Steps that we need to take to get this to work:
Term
s to Agda CoreTerm
s.Signature
to an Agda CoreGlobalScope
+Signature
for it.CompiledClauses
to an Agda CoreTerm
usingTCase
s for each node in the case tree.The text was updated successfully, but these errors were encountered: