Versions in this module Expand all Collapse all v0 v0.9.1 Oct 7, 2024 v0.9.0 Sep 7, 2024 v0.8.0 Sep 6, 2024 v0.7.1 Jul 20, 2024 v0.7.0 Jul 20, 2024 v0.6.2 Jul 20, 2024 v0.6.1 Jul 19, 2024 v0.6.0 Jul 19, 2024 Changes in this version + var LoopBreak = GallinaIdent("Break") + var LoopContinue = GallinaIdent("Continue") + var Null = nullLiteral + func ImportToPath(pkgPath, pkgName string) string + func InterfaceMethodName(interfaceName string, funcName string) string + func MethodName(tyName string, funcName string) string + type AliasDecl struct + Name string + Type Type + func (t AliasDecl) CoqDecl() string + type ArrayType struct + Elt Type + Len uint64 + func (t ArrayType) Coq(needs_paren bool) string + type ArrowType struct + ArgTypes []Type + ReturnType Type + func (t ArrowType) Coq(needs_paren bool) string + type BinOp int + const OpAnd + const OpAppend + const OpEquals + const OpGreaterEq + const OpGreaterThan + const OpLAnd + const OpLOr + const OpLessEq + const OpLessThan + const OpMinus + const OpMul + const OpNotEquals + const OpOr + const OpPlus + const OpQuot + const OpRem + const OpShl + const OpShr + const OpXor + type BinaryExpr struct + Op BinOp + X Expr + Y Expr + func (be BinaryExpr) Coq(needs_paren bool) string + type Binder *IdentExpr + type Binding struct + Expr Expr + Names []string + func NewAnon(e Expr) Binding + func (b Binding) AddTo(pp *buffer) + func (b Binding) Unwrap() (e Expr, ok bool) + type BlockExpr struct + Bindings []Binding + func (be BlockExpr) Coq(needs_paren bool) string + type BoolLiteral bool + var False BoolLiteral = false + var True BoolLiteral = true + func (b BoolLiteral) Coq(needs_paren bool) string + type ByteLiteral struct + Value uint8 + func (l ByteLiteral) Coq(needs_paren bool) string + type CallExpr struct + Args []Expr + MethodName Expr + TypeArgs []Expr + func NewCallExpr(name Expr, args ...Expr) CallExpr + func (s CallExpr) Coq(needs_paren bool) string + type CommentDecl string + func NewComment(s string) CommentDecl + func (d CommentDecl) CoqDecl() string + type ConstDecl struct + AddTypes bool + Comment string + Name string + Type Type + Val Expr + func (d ConstDecl) CoqDecl() string + type Decl interface + CoqDecl func() string + type DerefExpr struct + Ty Expr + X Expr + func (e DerefExpr) Coq(needs_paren bool) string + type Expr interface + Coq func(needs_paren bool) string + var Skip Expr = GallinaIdent("Skip") + func NewTuple(es []Expr) Expr + func StructDesc(name string) Expr + type FieldDecl struct + Name string + Type Type + func (d FieldDecl) Coq(needs_paren bool) string + func (d FieldDecl) CoqBinder() string + type File struct + Decls []Decl + Footer string + GoPackage string + ImportHeader string + Imports ImportDecls + PkgPath string + func (f File) Write(w io.Writer) + type ForLoopExpr struct + Body BlockExpr + Cond Expr + Init Binding + Post Expr + func (e ForLoopExpr) Coq(needs_paren bool) string + type FuncDecl struct + AddTypes bool + Args []FieldDecl + Body Expr + Comment string + Name string + ReturnType Type + TypeParams []TypeIdent + func (d FuncDecl) CoqDecl() string + func (d FuncDecl) Signature() string + func (d FuncDecl) Type() string + type FuncLit struct + Args []FieldDecl + Body Expr + func (e FuncLit) Coq(needs_paren bool) string + type FuncType struct + Params []string + Results []string + func (t FuncType) Coq(needs_paren bool) string + type GallinaIdent string + func (e GallinaIdent) Coq(needs_paren bool) string + type GallinaString string + func (s GallinaString) Coq(needs_paren bool) string + type HashTableInsert struct + Value Expr + func (e HashTableInsert) Coq(needs_paren bool) string + type IdentExpr string + func (e IdentExpr) Coq(needs_paren bool) string + type IfExpr struct + Cond Expr + Else Expr + Then Expr + func (ife IfExpr) Coq(needs_paren bool) string + type ImportDecl struct + Path string + Trusted bool + func (decl ImportDecl) CoqDecl() string + type ImportDecls []ImportDecl + func (decls ImportDecls) PrintImports() string + type Int32Literal struct + Value uint32 + func (l Int32Literal) Coq(needs_paren bool) string + type IntLiteral struct + Value uint64 + func (l IntLiteral) Coq(needs_paren bool) string + type InterfaceDecl struct + Comment string + Methods []FieldDecl + Name string + func (d InterfaceDecl) Coq(needs_paren bool) string + func (d InterfaceDecl) CoqDecl() string + type LoggingStmt struct + GoCall string + func (s LoggingStmt) Coq(needs_paren bool) string + type MapIterExpr struct + Body BlockExpr + KeyIdent string + Map Expr + ValueIdent string + func (e MapIterExpr) Coq(needs_paren bool) string + type MapType struct + Key Type + Value Type + func (t MapType) Coq(needs_paren bool) string + type NotExpr struct + X Expr + func (e NotExpr) Coq(needs_paren bool) string + type PackageIdent struct + Ident string + Package string + func (e PackageIdent) Coq(needs_paren bool) string + type PtrType struct + func (t PtrType) Coq(needs_paren bool) string + type RefExpr struct + Ty Expr + X Expr + func (e RefExpr) Coq(needs_paren bool) string + type ReturnExpr struct + Value Expr + func (e ReturnExpr) Coq(needs_paren bool) string + type SliceLoopExpr struct + Body BlockExpr + Key Binder + Slice Expr + Ty Expr + Val Binder + func (e SliceLoopExpr) Coq(needs_paren bool) string + type SliceType struct + Value Type + func (t SliceType) Coq(needs_paren bool) string + type SpawnExpr struct + Body BlockExpr + func (e SpawnExpr) Coq(needs_paren bool) string + type StoreStmt struct + Dst Expr + Ty Expr + X Expr + func (e StoreStmt) Coq(needs_paren bool) string + type StringLiteral struct + Value string + func (l StringLiteral) Coq(needs_paren bool) string + type StructDecl struct + Comment string + Fields []FieldDecl + Name string + func (d StructDecl) CoqDecl() string + type StructFieldAccessExpr struct + Field string + Struct string + ThroughPointer bool + X Expr + func (e StructFieldAccessExpr) Coq(needs_paren bool) string + type StructLiteral struct + Allocation bool + StructName string + func NewStructLiteral(structName string) StructLiteral + func (sl *StructLiteral) AddField(field string, value Expr) + func (sl StructLiteral) Coq(needs_paren bool) string + type StructName string + func (t StructName) Coq(needs_paren bool) string + type StructToInterface struct + Interface string + Methods []string + Struct string + func (d StructToInterface) Coq(needs_paren bool) string + func (d StructToInterface) CoqDecl() string + func (d StructToInterface) MethodList() []string + func (d StructToInterface) Name() string + type StructToInterfaceDecl struct + Arg string + Fun string + Interface string + Struct string + func (d StructToInterfaceDecl) Coq(needs_paren bool) string + type TupleExpr []Expr + func (te TupleExpr) Coq(needs_paren bool) string + type TupleType []Type + func (tt TupleType) Coq(needs_paren bool) string + type Type interface + Coq func(needs_paren bool) string + func NewTupleType(types []Type) Type + type TypeDef struct + Name string + Type Type + func (d TypeDef) CoqDecl() string + type TypeIdent string + func (t TypeIdent) Coq(needs_paren bool) string + type UnitLiteral struct + var Tt UnitLiteral = struct{}{} + func (tt UnitLiteral) Coq(needs_paren bool) string
Go to main page