New answers tagged proof-assistants
3
It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/...
Top 50 recent answers are included
