coq

package

Go to main page

Versions in this module

v0

v0.5.3

Mar 29, 2023

Changes in this version

type MapType

+ Key Type

v0.5.2

Dec 1, 2022

v0.5.1

Nov 29, 2022

Changes in this version

type ImportDecl

+ Trusted bool

v0.5.0

Jul 20, 2022

Changes in this version

type CallExpr

+ TypeArgs []Expr

type FuncDecl

+ TypeParams []TypeIdent

v0.4.5

Apr 30, 2022

Changes in this version

type File

+ Imports ImportDecls

type ImportDecls

+ func (decls ImportDecls) PrintImports() string

v0.4.4

Mar 30, 2022

v0.4.3

Mar 29, 2022

v0.4.2

Mar 20, 2022

v0.4.1

Dec 7, 2021

v0.4.0

Sep 23, 2021

v0.3.1

May 23, 2021

v0.3.0

May 23, 2021

Changes in this version

type File

+ PkgPath string

v0.2.0

May 18, 2021

v0.1.0

May 17, 2021

Changes in this version

+ var LoopBreak = GallinaIdent("Break")

+ var LoopContinue = GallinaIdent("Continue")

+ var Null = nullLiteral

+ func ImportToPath(importPath string) string

+ func InterfaceMethod(interfaceName string, methodName string) string

+ func StructMethod(structName string, methodName string) string

+ type ArrayType struct

+ Elt Type

+ Len uint64

+ func (t ArrayType) Coq() string

+ type ArrowType struct

+ ArgTypes []Type

+ ReturnType Type

+ func (t ArrowType) Coq() 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() 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() string

+ type BoolLiteral bool

+ var False BoolLiteral = false

+ var True BoolLiteral = true

+ func (b BoolLiteral) Coq() string

+ type ByteLiteral struct

+ Value uint8

+ func (l ByteLiteral) Coq() string

+ type CallExpr struct

+ Args []Expr

+ MethodName string

+ func NewCallExpr(name string, args ...Expr) CallExpr

+ func (s CallExpr) Coq() 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() string

+ type Expr interface

+ Coq func() 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() string

+ func (d FieldDecl) CoqBinder() string

+ type File struct

+ Decls []Decl

+ Footer string

+ GoPackage string

+ ImportHeader string

+ func (f File) Write(w io.Writer)

+ type ForLoopExpr struct

+ Body BlockExpr

+ Cond Expr

+ Init Binding

+ Post Expr

+ func (e ForLoopExpr) Coq() string

+ type FuncDecl struct

+ AddTypes bool

+ Args []FieldDecl

+ Body Expr

+ Comment string

+ Name string

+ ReturnType Type

+ 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() string

+ type FuncType struct

+ Params []string

+ Results []string

+ func (t FuncType) Coq() string

+ type GallinaIdent string

+ func (e GallinaIdent) Coq() string

+ type GallinaString string

+ func (s GallinaString) Coq() string

+ type HashTableInsert struct

+ Value Expr

+ func (e HashTableInsert) Coq() string

+ type IdentExpr string

+ func (e IdentExpr) Coq() string

+ type IfExpr struct

+ Cond Expr

+ Else Expr

+ Then Expr

+ func (ife IfExpr) Coq() string

+ type ImportDecl struct

+ Path string

+ func (decl ImportDecl) CoqDecl() string

+ type ImportDecls []ImportDecl

+ func (decls ImportDecls) CoqDecl() string

+ type Int32Literal struct

+ Value uint32

+ func (l Int32Literal) Coq() string

+ type IntLiteral struct

+ Value uint64

+ func (l IntLiteral) Coq() string

+ type InterfaceDecl struct

+ Comment string

+ Methods []FieldDecl

+ Name string

+ func (d InterfaceDecl) Coq() string

+ func (d InterfaceDecl) CoqDecl() string

+ type LoggingStmt struct

+ GoCall string

+ func (s LoggingStmt) Coq() string

+ type MapIterExpr struct

+ Body BlockExpr

+ KeyIdent string

+ Map Expr

+ ValueIdent string

+ func (e MapIterExpr) Coq() string

+ type MapType struct

+ Value Type

+ func (t MapType) Coq() string

+ type NotExpr struct

+ X Expr

+ func (e NotExpr) Coq() string

+ type PackageIdent struct

+ Ident string

+ Package string

+ func (e PackageIdent) Coq() string

+ type PtrType struct

+ Value Type

+ func (t PtrType) Coq() string

+ type RefExpr struct

+ Ty Expr

+ X Expr

+ func (e RefExpr) Coq() string

+ type ReturnExpr struct

+ Value Expr

+ func (e ReturnExpr) Coq() string

+ type SliceLoopExpr struct

+ Body BlockExpr

+ Key Binder

+ Slice Expr

+ Ty Expr

+ Val Binder

+ func (e SliceLoopExpr) Coq() string

+ type SliceType struct

+ Value Type

+ func (t SliceType) Coq() string

+ type SpawnExpr struct

+ Body BlockExpr

+ func (e SpawnExpr) Coq() string

+ type StoreStmt struct

+ Dst Expr

+ Ty Expr

+ X Expr

+ func (e StoreStmt) Coq() string

+ type StringLiteral struct

+ Value string

+ func (l StringLiteral) Coq() 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() 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() string

+ type StructName string

+ func (t StructName) Coq() string

+ type StructToInterface struct

+ Interface string

+ Methods []string

+ Struct string

+ func (d StructToInterface) Coq() 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() string

+ type TupleExpr []Expr

+ func (te TupleExpr) Coq() string

+ type TupleType []Type

+ func (tt TupleType) Coq() string

+ type Type interface

+ Coq func() string

+ func NewTupleType(types []Type) Type

+ type TypeDecl struct

+ Body Type

+ Name string

+ func (d TypeDecl) CoqDecl() string

+ type TypeIdent string

+ func (t TypeIdent) Coq() string

+ type UnitLiteral struct

+ var Tt UnitLiteral = struct{}{}

+ func (tt UnitLiteral) Coq() string

?	: This menu
/	: Search site
f or F	: Jump to
y or Y	: Canonical URL